Apply SNoLev_ind2 with λ x0 x1 . mul_SNo x0 x1 = mul_SNo x1 x0.

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Assume H1: SNo x1.

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

Assume H3: ∀ x2 . x2 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo x0 x2 = mul_SNo x2 x0.

Assume H4: ∀ x2 . x2 ∈ SNoS_ (SNoLev x0) ⟶ ∀ x3 . x3 ∈ SNoS_ (SNoLev x1) ⟶ mul_SNo x2 x3 = mul_SNo x3 x2.

Apply mul_SNo_eq_3 with x0, x1, mul_SNo x0 x1 = mul_SNo x1 x0 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H5: SNoCutP x2 x3.

Assume H6: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ (∀ x6 . x6 ∈ SNoR x0 ⟶ ∀ x7 . x7 ∈ SNoR x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ x5.

Assume H7: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x2.

Assume H8: ∀ x4 . x4 ∈ SNoR x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x2.

Assume H9: ∀ x4 . x4 ∈ x3 ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoR x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ (∀ x6 . x6 ∈ SNoR x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ x4 = add_SNo (mul_SNo x6 x1) (add_SNo (mul_SNo x0 x7) (minus_SNo (mul_SNo x6 x7))) ⟶ x5) ⟶ x5.

Assume H10: ∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ add_SNo (mul_SNo x4 x1) (add_SNo (mul_SNo x0 x5) (minus_SNo (mul_SNo x4 x5))) ∈ x3.

Assume H11: ∀ x4 . ... ⟶ ∀ x5 . ... ⟶ add_SNo (mul_SNo x4 x1) ... ∈ ....

...

■

Proofgold Proof