proposition: Lemma is_var_of_clause_cons : forall v l cl, is_var_of_clause v (l::cl) <-> var l = v \/ is_var_of_clause v cl.
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