Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι → ι be given.

Let x3 of type ι → ι → ι be given.

Assume H0: SNo x1.

Assume H1: ∀ x4 . x4 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x5 . SNo x5 ⟶ x2 x4 x5 = x3 x4 x5.

Assume H2: ∀ x4 . x4 ∈ SNoS_ (SNoLev x1) ⟶ x2 x0 x4 = x3 x0 x4.

Assume H3: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoL x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoL x1)}.

Assume H4: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoR x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoR x1)}.

Assume H5: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoR x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoL x0) (SNoR x1)}.

Assume H6: {add_SNo (x2 (ap x4 0) x1) (add_SNo (x2 x0 (ap x4 1)) (minus_SNo (x2 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoL x1)} = {add_SNo (x3 (ap x4 0) x1) (add_SNo (x3 x0 (ap x4 1)) (minus_SNo (x3 (ap x4 0) (ap x4 1))))|x4 ∈ setprod (SNoR x0) (SNoL x1)}.

Apply H3 with λ x4 x5 . SNoCut (binunion x5 {...|x6 ∈ setprod (SNoR x0) (SNoR x1)}) ... = ....

...

■

Proofgold Proof