proposition: Lemma wf_select_in_wmap : forall pos m g u cls (WFU: wf_units_lit u m) (WFW: WMap.wf cls) (WF : has_clauses m cls), ohold (check_annot has_conflict_clause m) (select_in_wmap pos u (is_classic g) cls) .
proof: Proof. intros. unfold select_in_wmap. destruct (WMap.search (select_clause (is_classic g) u) pos cls) eqn:EQ; [|simpl; tauto]. apply WMap.search_correct with (P := fun cl => check_annot has_watched_clause m cl) in EQ; auto. destruct EQ as (k&v&P&S). rewrite <- S. apply check_annot_select_clause; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause