| ∀ x0 : ι → ι → (ι → ι → ι) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 . (∀ x5 . SNo x5 ⟶ ∀ x6 . SNo x6 ⟶ ∀ x7 x8 : ι → ι → ι . (∀ x9 . x9 ∈ SNoS_ (SNoLev x5) ⟶ ∀ x10 . SNo x10 ⟶ x7 x9 x10 = x8 x9 x10) ⟶ (∀ x9 . x9 ∈ SNoS_ (SNoLev x6) ⟶ x7 x5 x9 = x8 x5 x9) ⟶ x0 x5 x6 x7 = x0 x5 x6 x8) ⟶ (∀ x5 . x5 ∈ SNoS_ (SNoLev x1) ⟶ x2 x5 = x3 x5) ⟶ SNo x4 ⟶ (∀ x5 . ordinal x5 ⟶ ∀ x6 . x6 ∈ SNoS_ x5 ⟶ SNo_rec_i (λ x8 . λ x9 : ι → ι . x0 x1 x8 (λ x10 x11 . If_i (x10 = x1) (x9 x11) (x2 x10 x11))) x6 = SNo_rec_i (λ x8 . λ x9 : ι → ι . x0 x1 x8 (λ x10 x11 . If_i (x10 = x1) (x9 x11) (x3 x10 x11))) x6) ⟶ SNo_rec_i (λ x6 . λ x7 : ι → ι . x0 x1 x6 (λ x8 x9 . If_i (x8 = x1) (x7 x9) (x2 x8 x9))) x4 = SNo_rec_i (λ x6 . λ x7 : ι → ι . x0 x1 x6 (λ x8 x9 . If_i (x8 = x1) (x7 x9) (x3 x8 x9))) x4 |
|