Require Export ST.

Section Uncountable.

  (* We assume a countable model containing a set omega
     that is an injective image of nat *)

  Variable set : SetStruct.
  Variable ZFS : ZF set.

  Variable f : nat -> set.
  Variable f_sur : forall x, exists n, f n = x.

  Variable num : nat -> set.
  Variable num_inj : forall m n, num m = num n -> m = n.

  Definition Num x :=
    exists n, x = num n.

  Variable ident omega : set.
  Variable Inf : agree Num omega.

  (* With a diagonalisation argument we derive a contradiction *)

  Definition N n :=
    (num n) nel (f n).

  Definition M :=
    omega ! fun x => exists n, num n = x /\ N n.

  Lemma help n :
    f n = M -> (num n nel M <-> (num n el omega /\ (exists m, num m = num n /\ N m))).
  Proof.
    intros H. split; intros I.
    - split.
      + apply Inf. now exists n.
      + exists n. split; trivial. unfold N. now rewrite H.
    - intros J. destruct I as [I1[m[I2 I3]]].
      apply I3. apply num_inj in I2. subst m. now rewrite H.
  Qed.

  Lemma false :
    False.
  Proof.
    destruct (f_sur M) as [n H].
    specialize (sep_el omega (fun x => exists n, num n = x /\ N n)).
    intros I. specialize (I (num n)). fold N in I.
    apply help in H. tauto.
  Qed.

End Uncountable.