Let w and u be given.

Assume H1: u ∈ {Unj z|z ∈ w, ∃x : set, Inj0 x = z}.

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

We will prove Inj0 u ∈ w.

Apply (ReplSepE_impred w (λz ⇒ ∃x : set, Inj0 x = z) Unj u H1) to the current goal.

Let z be given.

Assume H2: z ∈ w.

Assume H3: ∃x, Inj0 x = z.

Assume H4: u = Unj z.

Apply H3 to the current goal.

Let x be given.

Assume H5: Inj0 x = z.

We will prove Inj0 u ∈ w.

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

We will prove Inj0 (Unj z) ∈ w.

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

We will prove Inj0 (Unj (Inj0 x)) ∈ w.

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

We will prove Inj0 x ∈ w.

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

An exact proof term for the current goal is H2.

∎