proposition: Lemma vars_of_cnf_nil : forall cls, vars_of_cnf cls = nil -> cls = List.map (fun _ => nil) cls.
proof: Proof. induction cls. - simpl. reflexivity. - simpl. intros. apply app_eq_nil in H. destruct H as [H1 H2]. apply vars_of_clause_nil in H1. apply IHcls in H2. subst a. rewrite <- H2. reflexivity. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause