Let x0 of type ι → ι → CT2 ι be given.
Assume H0:
∀ x1 . SNo x1 ⟶ ∀ x2 . SNo x2 ⟶ ∀ x3 x4 : ι → ι → ι . (∀ x5 . x5 ∈ SNoS_ (SNoLev x1) ⟶ ∀ x6 . SNo x6 ⟶ x3 x5 x6 = x4 x5 x6) ⟶ (∀ x5 . x5 ∈ SNoS_ (SNoLev x2) ⟶ x3 x1 x5 = x4 x1 x5) ⟶ x0 x1 x2 x3 = x0 x1 x2 x4.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Assume H2:
∀ x4 . x4 ∈ SNoS_ (SNoLev x1) ⟶ x2 x4 = x3 x4.
Let x4 of type ι be given.
Let x5 of type ι → ι be given.
Let x6 of type ι → ι be given.
Assume H4:
∀ x7 . x7 ∈ SNoS_ (SNoLev x4) ⟶ x5 x7 = x6 x7.
Apply H0 with
x1,
x4,
λ x7 x8 . If_i (x7 = x1) (x5 x8) (x2 x7 x8),
λ x7 x8 . If_i (x7 = x1) (x6 x8) (x3 x7 x8) leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x7 of type ι be given.
Let x8 of type ι be given.
Claim L7: x7 = x1 ⟶ ∀ x9 : ο . x9
Apply SNoS_In_neq with
x1,
x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply If_i_0 with
x7 = x1,
x5 x8,
x2 x7 x8,
λ x9 x10 . x10 = If_i (x7 = x1) (x6 x8) (x3 x7 x8) leaving 2 subgoals.
The subproof is completed by applying L7.
Apply If_i_0 with
x7 = x1,
x6 x8,
x3 x7 x8,
λ x9 x10 . x2 x7 x8 = x10 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply H2 with
x7,
λ x9 x10 : ι → ι . x10 x8 = x3 x7 x8 leaving 2 subgoals.
The subproof is completed by applying H5.
Let x9 of type ι → ι → ο be given.
Assume H8: x9 (x3 x7 x8) (x3 x7 x8).
The subproof is completed by applying H8.
Let x7 of type ι be given.
Apply If_i_1 with
x1 = x1,
x5 x7,
x2 x1 x7,
λ x8 x9 . x9 = If_i (x1 = x1) (x6 x7) (x3 x1 x7) leaving 2 subgoals.
Let x8 of type ι → ι → ο be given.
Assume H6: x8 x1 x1.
The subproof is completed by applying H6.
Apply If_i_1 with
x1 = x1,
x6 x7,
x3 x1 x7,
λ x8 x9 . x5 x7 = x9 leaving 2 subgoals.
Let x8 of type ι → ι → ο be given.
Assume H6: x8 x1 x1.
The subproof is completed by applying H6.
Apply H4 with
x7.
The subproof is completed by applying H5.