proposition: Lemma is_var_of_clause_nil : forall v, is_var_of_clause v nil <-> False.
proof: Proof. unfold is_var_of_clause. simpl. firstorder congruence. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause