Let X and y be given.

Assume HX H1.

We prove the intermediate claim L1: {- z|z ∈ {- x|x ∈ X}} = X.

Apply Repl_invol_eq SNo minus_SNo to the current goal.

We will prove ∀x, SNo x → - - x = x.

An exact proof term for the current goal is minus_SNo_invol.

We will prove ∀x ∈ X, SNo x.

An exact proof term for the current goal is HX.

We prove the intermediate claim L2: ∀z ∈ {- x|x ∈ X}, SNo z.

Let z be given.

Assume Hz.

Apply ReplE_impred X (λx ⇒ - x) z Hz to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Assume Hzx: z = - x.

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

Apply SNo_minus_SNo to the current goal.

We will prove SNo x.

An exact proof term for the current goal is HX x Hx.

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

An exact proof term for the current goal is minus_SNo_max_min {- x|x ∈ X} y L2 H1.

∎