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.