proposition: Lemma is_var_of_cnf_merge : forall v a l2, is_var_of_cnf v (map (Elim.merge_clause a) l2) -> is_var_of_clause v a \/ is_var_of_cnf v l2.
proof: Proof. induction l2. - simpl. rewrite is_var_of_cnf_nil. tauto. - simpl. rewrite! is_var_of_cnf_cons. rewrite! is_var_of_clause_merge. rewrite! is_var_of_clause_app. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause