| ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ setminus x1 (Sing x3) ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ 323f1.. x2 x4 x5 x6 x7 x8 x9 x10 ⟶ ∀ x11 : ο . (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ afd75.. x2 x12 x13 x14 x3 x15 x16 x17 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ e1b03.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 5f483.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 1610e.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 0282b.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 6a4fb.. x2 x12 x13 x14 x15 x16 x17 x3 x18 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 599ac.. x2 x12 x13 x14 x15 x16 x17 x18 x3 ⟶ x11) ⟶ (∀ x12 . x12 ∈ x0 ⟶ ∀ x13 . x13 ∈ x0 ⟶ ∀ x14 . x14 ∈ x0 ⟶ ∀ x15 . x15 ∈ x0 ⟶ ∀ x16 . x16 ∈ x0 ⟶ ∀ x17 . x17 ∈ x0 ⟶ ∀ x18 . x18 ∈ x0 ⟶ 6caef.. x2 x3 x12 x13 x14 x15 x16 x17 x18 ⟶ x11) ⟶ x11 |
|