proposition: Lemma is_var_of_cnf_app : forall v cl1 cl2, is_var_of_cnf v (cl1 ++cl2) <-> (is_var_of_cnf v cl1 \/ is_var_of_cnf v cl2).
proof: Proof. induction cl1. - intros. simpl. rewrite is_var_of_cnf_nil. tauto. - intros. simpl. rewrite !is_var_of_cnf_cons. rewrite IHcl1. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause