Let c and r be given.
Assume Hc Hr.
We will prove {p ∈ EuclidPlane|Rlt (distance_R2 p c) r} ∈ circular_regions.
We prove the intermediate claim HPow: {p ∈ EuclidPlane|Rlt (distance_R2 p c) r} ∈ 𝒫 EuclidPlane.
Apply PowerI EuclidPlane {p ∈ EuclidPlane|Rlt (distance_R2 p c) r} to the current goal.
Let p be given.
Assume Hp.
An exact proof term for the current goal is (SepE1 EuclidPlane (λp0 : set ⇒ Rlt (distance_R2 p0 c) r) p Hp).
We prove the intermediate claim HPred: ∃c0 : set, ∃r0 : set, c0 ∈ EuclidPlane ∧ Rlt 0 r0 ∧ {p ∈ EuclidPlane|Rlt (distance_R2 p c) r} = {p ∈ EuclidPlane|Rlt (distance_R2 p c0) r0}.
We use c to witness the existential quantifier.
We use r to witness the existential quantifier.
Apply and3I to the current goal.
An exact proof term for the current goal is Hc.
An exact proof term for the current goal is Hr.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 EuclidPlane) (λU0 : set ⇒ ∃c0 : set, ∃r0 : set, c0 ∈ EuclidPlane ∧ Rlt 0 r0 ∧ U0 = {p ∈ EuclidPlane|Rlt (distance_R2 p c0) r0}) {p ∈ EuclidPlane|Rlt (distance_R2 p c) r} HPow HPred).
∎