Let x be given.

Assume Hx: x ∈ K_set.

Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ inv_nat n) x Hx (x ∈ R)) to the current goal.

Let n be given.

Assume HnIn: n ∈ ω ∖ {0}.

Assume Heq: x = inv_nat n.

We prove the intermediate claim HnO: n ∈ ω.

An exact proof term for the current goal is (setminusE1 ω {0} n HnIn).

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

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

∎