proposition: Lemma not_make_conj_app : forall (A:Type) (t:list A) a eval (no_middle_eval : forall d, eval d \/ ~ eval d) , ~ make_conj eval (t ++ a) <-> (~ make_conj eval t) \/ (~ make_conj eval a).
proof: Proof. intros A t; induction t as [|a t IHt]. - simpl. tauto. - intros a0 **. simpl ((a::t)++a0). rewrite !not_make_conj_cons by auto. rewrite IHt by auto. tauto. Qed.
imports: List