proposition: Lemma type_discr2 : forall A B C, ~A = (A --> B) --> C.
proof: Proof. induction A; unfold not; simpl; intros. discr. unfold not in *. inversion H. eapply IHA1. apply H1. Qed.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)