Cantors Diagonalization Proof in Coq

Axiom b : (nat -> nat) -> nat.
Axiom b' : nat -> (nat -> nat).

Axiom bijection : forall f, b' (b f) = f.
Axiom bijection' : forall x, b (b' x) = x.

Definition Stream A := nat -> A.
Definition Map {A B} (f : A -> B) : Stream A -> Stream B :=
  fun sa =>
    fun i =>
      f (sa i).

Definition l : Stream (nat -> nat) -> Stream nat :=
  Map b.
Definition l' : Stream nat -> Stream (nat -> nat) :=
  Map b'.

Definition isnt x :=
  match x with
    | O => S O
    | S _ => O
  end.

Theorem isn't_isnt {x} : isnt x <> x.
  destruct x; discriminate.
Qed.

Definition Diagonal {A} (s : Stream (Stream A)) : Stream A:=
  fun i => s i i.

Definition Diagonalization (sequences : Stream (nat -> nat)) : Stream nat :=
  Map isnt (Diagonal sequences).

Theorem isn't_in {sequences} : forall i, Diagonalization sequences <> sequences i.
intros; intro.
pose (f_equal (fun f => f i) H) as H'.
unfold Diagonalization in H'.
unfold Diagonal in H'.
unfold Map in H'.
revert H'.
apply isn't_isnt.
Qed.

Definition pink_elephant : Stream nat := fun i => i.

Definition sequence_enumeration : Stream (nat -> nat) := l' pink_elephant.

Theorem every_sequence : forall s, exists i, s = sequence_enumeration i.
intro s; exists (b s).
unfold sequence_enumeration.
unfold pink_elephant.
unfold l'.
unfold Map.
rewrite bijection.
reflexivity.
Qed.

Theorem Cantor : False.
destruct (every_sequence (Diagonalization sequence_enumeration)) as [i iPrf].
pose (@isn't_in sequence_enumeration i).
contradiction.
Qed.