Library cantor

Definition enumeration: Type := nat -> (nat-> nat).
Definition diagonal (g: enumeration) (n: nat): nat := g n n.
Definition different (f: nat->nat) (g: nat->nat): Prop := exists n: nat, f(n)<>g(n).

Theorem cantor : forall g: enumeration, exists f: nat->nat,
   forall i: nat, different (g i) f.
intro. (* Let g be an enumeration of all functions. *)
exists (fun k=>S(diagonal g k)).
intro. (* Let i be a row--an element of the enumeration. *)
exists i.
auto.
Qed.