proposition: Lemma eval_find_split : forall 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) (find_split u (is_classic g) cls) -> eval_ohformula g), eval_ohformula g.
proof: Proof. intros. unfold find_split in EVAL. revert EVAL. destruct_in_goal SEL. rewrite <- SEL. eapply eval_select_in_wmap; eauto. eapply eval_select_in_wmap; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause