proposition: Lemma not_make_conj_cons : forall (A:Type) (t:A) a eval (no_middle_eval : (eval t) \/ ~ (eval t)), ~ make_conj eval (t ::a) <-> ~ (eval t) \/ (~ make_conj eval a).
proof: Proof. intros. rewrite make_conj_cons. tauto. Qed.
imports: List