proposition: Lemma cantor_diag2: forall (X:Type) (f:X->(X->Prop)), ~ surjective f.
proof: Proof. unfold not; intros. pose (g := fun x:X => ~ f x x). pose proof (H g). destruct H0. assert (f x x = g x). rewrite H0. reflexivity. unfold g in H1. contradiction P_neq_not_P with (f x x). Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec