+
+
+include "topology/igft.ma".
+
+ninductive unit : Type[0] ≝ one : unit.
+
+naxiom E: setoid.
+naxiom R: E → Ω^E.
+
+ndefinition axs: Ax.
+@ E (λ_.unit) (λa,x.R a);
+nqed.
+
+unification hint 0 ≔ ;
+ x ≟ axs
+ (* -------------- *) ⊢
+ S x ≡ E.
+
+ndefinition emptyset: Ω^axs ≝ {x | False}.
+
+ndefinition Z: Ω^axs ≝ {x | x ◃ emptyset}.
+
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+alias symbol "covers" = "covers".
+alias symbol "covers" = "covers set".
+ntheorem cover_trans: ∀A:Ax.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+#A; #a; #U; #V; #aU; #UV;
+nelim aU;
+##[ #c; #H; napply (UV … H);
+##| #c; #i; #HCU; #H; napply (cinfinity … i); napply H;
+##]
+nqed.
+
+ntheorem cantor: ∀a:axs. ¬ (Z ⊆ R a ∧ R a ⊆ Z).
+#a; *; #ZRa; #RaZ;
+ncut (a ◃ R a); ##[ @2; ##[ napply one; ##] #x; #H; @; napply H; ##] #H1;
+ncut (a ◃ emptyset); ##[
+ napply (cover_trans … H1);
+ #x; #H; nlapply (RaZ … H); #ABS; napply ABS; ##] #H2;
+ncut (a ∈ R a); ##[ napply ZRa; napply H2; ##] #H3;
+nelim H2 in H3;
+##[ nauto.
+##| nnormalize; nauto. ##] (* se lo lancio su entrambi fallisce di width *)
+nqed.
+