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

Let x be given.

We will prove x ∈ X.

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

Let y be given.

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

Assume H3: x = Unj y.

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

We will prove Unj y ∈ X.

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

Assume H4: y ∈ Inj1 X.

Assume H5: y ∉ {0}.

Apply (Inj1E X y H4) to the current goal.

Assume H6: y = 0.

We will prove False.

Apply H5 to the current goal.

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

We will prove 0 ∈ {0}.

Apply SingI to the current goal.

Assume H6: ∃x ∈ X, y = Inj1 x.

Apply (exandE_i (λx ⇒ x ∈ X) (λx ⇒ y = Inj1 x) H6) to the current goal.

Let z be given.

Assume H7: z ∈ X.

Assume H8: y = Inj1 z.

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

We will prove Unj (Inj1 z) ∈ X.

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

We will prove z ∈ X.

An exact proof term for the current goal is H7.

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

Let x be given.

Assume H1: x ∈ X.

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

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

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

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

Apply setminusI to the current goal.

An exact proof term for the current goal is (Inj1I2 X x H1).

We will prove Inj1 x ∉ {0}.

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