proposition: Lemma is_var_of_cnf_resolve : forall v l1 l2, is_var_of_cnf v (Elim.resolve_all l1 l2) -> is_var_of_cnf v (l1++ l2).
proof: Proof. induction l1;simpl. - intros. rewrite is_var_of_cnf_nil in H. tauto. - intros. rewrite is_var_of_cnf_app in H. destruct H. + rewrite is_var_of_cnf_cons. rewrite or_comm. rewrite is_var_of_cnf_app. rewrite or_assoc. right. apply is_var_of_cnf_normalise in H. apply is_var_of_cnf_merge in H. tauto. + apply IHl1 in H. rewrite is_var_of_cnf_cons. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause