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

Let w and u be given.

Assume H1: Inj0 u ∈ w.

We will prove u ∈ {Unj z|z ∈ w, ∃x : set, Inj0 x = z}.

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

We will prove Unj (Inj0 u) ∈ {Unj z|z ∈ w, ∃x : set, Inj0 x = z}.

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

We will prove Inj0 u ∈ w.

An exact proof term for the current goal is H1.

We will prove ∃x, Inj0 x = Inj0 u.

We use u to witness the existential quantifier.

Use reflexivity.

∎