proposition: Lemma cantor_diag: forall (X:Type) (f:X->(X->bool)), ~ surjective f.
proof: Proof. intros. red; intro. pose (g := fun x:X => negb (f x x)). pose proof (H g). destruct H0. assert (f x x = g x). rewrite H0. reflexivity. unfold g in H1. destruct (f x x). discriminate H1. discriminate H1. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec