proposition: Lemma is_var_of_cnf_nil : forall v, is_var_of_cnf v nil <-> False.
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