(* Argument diagonal de Cantor *) Definition Ensemble (A:Type) := A-> Prop. Definition surjection (A B : Type)(f:A-> B) := forall b:B, exists a:A, f a = b. Section Kantor. Variable A : Set. Definition elem a (A:Ensemble A) := A a. Definition set_of (Pred : A -> Prop) : Ensemble A := Pred. Hypothesis surj: exists f:A->Ensemble A, surjection A (Ensemble A) f. Theorem Kantors_Diagonal : False. Proof. elim surj;intros f Hf. (* permet d'introduire une definition locale dans une preuve *) pose (X := set_of (fun a => ~elem a (f a))). elim (Hf X). intros b Hb. assert (~ elem b (f b)). rewrite Hb. intro n. absurd (elem b (f b)). apply n. rewrite Hb;auto. elim H. rewrite Hb. unfold X. unfold elem, set_of. auto. Qed. End Kantor.