proposition: Lemma wf_find_split : forall 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) (find_split u (is_classic g) cls) .
proof: Proof. intros. unfold find_split. destruct_in_goal SEL. rewrite <- SEL. apply wf_select_in_wmap ; auto. apply wf_select_in_wmap ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause