proposition: Lemma is_var_of_cnf_False : forall cls, (forall v , is_var_of_cnf v cls -> False) -> forall cl, In cl cls -> cl = nil.
proof: Proof. intros. induction cls. - simpl. firstorder. - simpl in H0. destruct H0; subst. destruct cl;auto. exfalso. apply (H (var t)). rewrite is_var_of_cnf_cons. left. rewrite is_var_of_clause_cons. tauto. eapply IHcls; auto. intros. apply (H v). rewrite is_var_of_cnf_cons. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause