proposition: Lemma is_var_of_cnf_cons : forall v c cls, is_var_of_cnf v (c :: cls) <-> (is_var_of_clause v c \/ is_var_of_cnf v cls).
proof: Proof. unfold is_var_of_cnf at 1. intros. simpl. firstorder congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause