We will prove Hausdorff_space R_K R_K_topology ∧ ¬ regular_space R_K R_K_topology.
Apply andI to the current goal.
We prove the intermediate claim HRKeq: R_K = R.
Use reflexivity.
rewrite the current goal using HRKeq (from left to right).
An exact proof term for the current goal is R_K_topology_Hausdorff.
An exact proof term for the current goal is RK_not_regular_axiom.
∎