proposition: Lemma vars_of_cnf_uniq : forall p cls, (forall x , In x (vars_of_cnf cls) -> x = p) -> forall cl : clause, In cl cls -> is_clause_of p cl.
proof: Proof. induction cls. - intros. simpl in H0. tauto. - intros. simpl in H0. simpl in H. destruct H0 ; subst. assert ((forall x, In x (vars_of_clause cl) -> x = p)). { intros. apply H. rewrite in_app_iff. tauto. } clear H IHcls. unfold is_clause_of. intros. unfold vars_of_clause in H0. apply H0. rewrite in_map_iff. exists l; simpl;auto. eapply IHcls;eauto. intros. apply H. rewrite in_app_iff. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause