proposition: Lemma vars_of_cnf_ok : forall cls v, is_var_of_cnf v cls <-> In v (vars_of_cnf cls).
proof: Proof. unfold is_var_of_cnf, vars_of_cnf,vars_of_clause. induction cls;simpl;intros. - split; firstorder. - rewrite in_app_iff. rewrite <- IHcls. rewrite in_map_iff. firstorder congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause