Let u be given.

Assume Hu: u ∈ U.

Apply (ReplE_impred X (λx0 : set ⇒ open_ball X d x0 (inv_nat (ordsucc n))) u Hu (u ∈ Tx)) to the current goal.

Let x0 be given.

Assume Hx0X: x0 ∈ X.

Assume HuEq: u = open_ball X d x0 (inv_nat (ordsucc n)).

rewrite the current goal using HuEq (from left to right).

We prove the intermediate claim Hn1O: ordsucc n ∈ ω.

An exact proof term for the current goal is (omega_ordsucc n HnO).

We prove the intermediate claim Hn1NZ: ordsucc n ∈ ω ∖ {0}.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hn1O.

Assume Hmem0: ordsucc n ∈ {0}.

We prove the intermediate claim Heq0: ordsucc n = 0.

An exact proof term for the current goal is (SingE 0 (ordsucc n) Hmem0).

An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).

We prove the intermediate claim Hrpos: Rlt 0 (inv_nat (ordsucc n)).

An exact proof term for the current goal is (inv_nat_pos (ordsucc n) Hn1NZ).

An exact proof term for the current goal is (open_ball_in_metric_topology X d x0 (inv_nat (ordsucc n)) Hm Hx0X Hrpos).

Let x be given.

Assume HxX: x ∈ X.

We will prove ∃u : set, u ∈ U ∧ x ∈ u.

We use (open_ball X d x (inv_nat (ordsucc n))) to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ open_ball X d x0 (inv_nat (ordsucc n))) x HxX).