proposition: Lemma exc_intro_class : forall (A:Type) (P:A->Prop), ((forall x, ~P x) -> False) -> exc P.
proof: Proof. intros; apply class_exc; red; intros. apply H; red; intros; auto. apply H0; apply exc_intro with (x:=x);auto. Qed.