proposition: Lemma intro_impl_correct : forall m f hf l o (WF: has_form m hf) (EQ: hf.(elt) = f), intro_impl nil f hf = (l,o) -> (Forall eval_literal l -> eval_ohformula o) <-> eval_formula f.
proof: Proof. intros. apply intro_impl_aux with (m:=m) in H ; auto. rewrite (Forall_rew nil) in H. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause