proposition: Lemma wf_cnf_of_literal : forall m l b cp cm ar acc f hf m' ar' w (HA : Forall (has_literal m) ar) (ACC: Forall (has_watched_clause m) acc) (HFF :elt hf = f) (HF : has_form m hf) (EQ : cnf_of_literal l b cp cm ar acc f hf = (m',ar',w)), Forall (has_literal m) ar' /\ Forall (has_watched_clause m) w.
proof: Proof. unfold cnf_of_literal. intros. apply wf_cnf with (m:=m) in EQ ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause