proposition: Lemma class_exc : forall (A :Type)(P:A->Prop), class (exc P).
proof: Proof. repeat red; intros. apply H0; clear H0; red; intro. apply H; clear H; red; intro H2. apply H2; intros; auto. apply H0; apply (H1 x); auto. Qed.