proposition: Lemma classic_excluded_middle: classic -> excluded_middle.
proof: Proof. unfold excluded_middle; intros H P. apply H; intro H0; absurd P. - intro H1; apply H0 ; now left. - apply H; intro H1; apply H0; now right. Qed.