proposition: Lemma search_correct : forall P b m r (WFE : wf m) (ALL: Forall P m) (S : search b m = Some r), exists k c, P c /\ select k c = Some r.
proof: Proof. unfold search. intros. apply IntMap.search_some with (opt:= None) in S; auto. destruct S as (k&v&G&S). assert (G':= G). apply ALL in G. destruct G as (GF & GS). apply WFE in G'. destruct G' as (WFF & WFS). unfold search_in_pair_map in S. destruct b. - unfold search_in_map in S. apply IntMap.search_some with (opt:= None) in S; auto. destruct S as (k' & v' & G2 & S2). exists k', v'; split; auto. apply GS in G2 ; auto. - unfold search_in_map in S. apply IntMap.search_some with (opt:= None) in S; auto. destruct S as (k' & v' & G2 & S2). exists k', v'; split; auto. apply GF in G2 ; auto. - destruct WFE; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause