Assume Heq: unit_interval = R.
We will prove False.
We prove the intermediate claim H2I: 2 ∈ unit_interval.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is two_in_R.
An exact proof term for the current goal is (two_not_in_unit_interval H2I).
∎