We will prove {Unj x|x ∈ Inj0 X ∖ {0}} ⊆ X.

Let x be given.

We will prove x ∈ X.

Apply (ReplE_impred (Inj0 X ∖ {0}) Unj x H1) to the current goal.

Let y be given.

Assume H2: y ∈ Inj0 X ∖ {0}.

Assume H3: x = Unj y.

Apply (setminusE (Inj0 X) {0} y H2) to the current goal.

Assume H4: y ∈ {Inj1 x|x ∈ X}.

Assume H5: y ∉ {0}.

Apply (ReplE_impred X Inj1 y H4) to the current goal.

Let z be given.

Assume H6: z ∈ X.

Assume H7: y = Inj1 z.

We prove the intermediate claim L1: x = z.

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

We will prove Unj y = z.

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

We will prove Unj (Inj1 z) = z.

An exact proof term for the current goal is (Unj_Inj1_eq z).

We will prove x ∈ X.

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

We will prove z ∈ X.

An exact proof term for the current goal is H6.

We will prove X ⊆ {Unj x|x ∈ Inj0 X ∖ {0}}.

Let x be given.

Assume H1: x ∈ X.

We will prove x ∈ {Unj x|x ∈ Inj0 X ∖ {0}}.

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

Apply (ReplI (Inj0 X ∖ {0}) Unj) to the current goal.

We will prove Inj1 x ∈ Inj0 X ∖ {0}.

Apply setminusI to the current goal.

We will prove Inj1 x ∈ {Inj1 x|x ∈ X}.

Apply ReplI to the current goal.

An exact proof term for the current goal is H1.

We will prove Inj1 x ∉ {0}.

An exact proof term for the current goal is (Inj1NE2 x).