Let w and u be given.

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

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

We will prove Inj1 u ∈ w.

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

Let z be given.

Assume H2: z ∈ w.

Assume H3: ∃y, Inj1 y = z.

Assume H4: u = Unj z.

Apply H3 to the current goal.

Let y be given.

Assume H5: Inj1 y = z.

We will prove Inj1 u ∈ w.

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

We will prove Inj1 (Unj z) ∈ w.

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

We will prove Inj1 (Unj (Inj1 y)) ∈ w.

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

We will prove Inj1 y ∈ w.

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

An exact proof term for the current goal is H2.

∎