+nqed.
+
+nrecord Pt (A: Ax_pro) : Type[1] ≝
+ { pt_set: Ω^A;
+ pt_inhabited: ∃a. a ∈ pt_set;
+ pt_filtering: ∀a,b. a ∈ pt_set → b ∈ pt_set → ∃c. c ∈ (singleton … a) ↓ (singleton … b) → c ∈ pt_set;
+ pt_closed: pt_set ⊆ {b | b ⋉ pt_set}
+ }.
+
+ndefinition Rd ≝ Pt Rax.
+
+naxiom daemon: False.
+
+ndefinition Q_to_R: Q → Rd.
+ #q; @
+ [ napply { c | fst … c < q ∧ q < snd … c }
+ | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ]
+##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon]
+##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/
+ [ ncases daemon; ##| #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
+ [ #w; nnormalize; ncases daemon;
+ ##| nnormalize; ncases daemon;
+##]
+nqed.
+