proposition: Lemma vars_of_clause_ok : forall p cl, is_var_of_clause p cl <-> In p (vars_of_clause cl).
proof: Proof. induction cl. - rewrite is_var_of_clause_nil. simpl. tauto. - rewrite is_var_of_clause_cons. simpl. rewrite IHcl. tauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause