proposition: Theorem Eeq_implies_Req_realizer : forall e, Eeq_implies_Req↓e ⊩ ∀x y, Cauchy x → (x ≡≡ y → x ≡ y)%Re.
proof: Proof. Kmove. exists ε₁. find. repeat Ksolve. eok. now split. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions