We will prove topologists_sine_curve ⊆ EuclidPlane.
We prove the intermediate claim Hex: ∃S : set, S ⊆ EuclidPlane.
We use Empty to witness the existential quantifier.
An exact proof term for the current goal is (Subq_Empty EuclidPlane).
An exact proof term for the current goal is (Eps_i_ex (λS : set ⇒ S ⊆ EuclidPlane) Hex).
∎