proposition: Lemma eval_select_in_wmap : forall pos m g u cls (WFW: WMap.wf cls) (WFU: wf_units_lit u m) (EU : eval_units m u) (WF : has_clauses m cls) (EV : eval_clauses cls) (EVAL : ohold (Annot.lift eval_or) (select_in_wmap pos u (is_classic g) cls) -> eval_ohformula g), eval_ohformula g.
proof: Proof. intros. unfold select_in_wmap in EVAL. revert EVAL. destruct (WMap.search (select_clause (is_classic g) u) pos cls) eqn:EQ; [|simpl; tauto]. apply WMap.search_correct with (P := fun cl => Annot.lift eval_watched_clause cl /\ check_annot has_watched_clause m cl) in EQ; auto. destruct EQ as (k&v&P&S). rewrite <- S. destruct P as (P1 & P2). eapply eval_select_clause; eauto. apply WMap.ForallAND; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause