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

Let w and u be given.

Assume H1: Inj1 u ∈ w.

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

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

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

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

We will prove Inj1 u ∈ w.

An exact proof term for the current goal is H1.

We will prove ∃y, Inj1 y = Inj1 u.

We use u to witness the existential quantifier.

Use reflexivity.

∎