| ∀ x0 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ∈ x1 ⟶ x2 x3 x4 ⟶ x2 x4 x3) ⟶ 4402e.. x1 x2 ⟶ cf2df.. x1 x2 ⟶ ∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ⊆ setminus x1 (Sing x3) ⟶ ∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x4 ⟶ ∀ x10 . x10 ∈ x4 ⟶ ∀ x11 . x11 ∈ x4 ⟶ ∀ x12 . x12 ∈ x4 ⟶ ∀ x13 . x13 ∈ x4 ⟶ x0 x2 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ 5bab1.. x1 x2) ⟶ ∀ x1 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4) ⟶ 4402e.. x2 x3 ⟶ cf2df.. x2 x3 ⟶ ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ⊆ setminus x2 (Sing x4) ⟶ ∀ x6 . x6 ∈ x5 ⟶ ∀ x7 . x7 ∈ x5 ⟶ ∀ x8 . x8 ∈ x5 ⟶ ∀ x9 . x9 ∈ x5 ⟶ ∀ x10 . x10 ∈ x5 ⟶ ∀ x11 . x11 ∈ x5 ⟶ ∀ x12 . x12 ∈ x5 ⟶ ∀ x13 . x13 ∈ x5 ⟶ ∀ x14 . x14 ∈ x5 ⟶ x1 x3 x6 x7 x8 x9 x10 x11 x12 x13 x14 ⟶ 5bab1.. x2 x3) ⟶ ∀ x2 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x3 . ∀ x4 : ι → ι → ο . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5) ⟶ 4402e.. x3 x4 ⟶ cf2df.. x3 x4 ⟶ ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ⊆ setminus x3 (Sing x5) ⟶ ∀ x7 . x7 ∈ x6 ⟶ ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ ∀ x10 . x10 ∈ x6 ⟶ ∀ x11 . x11 ∈ x6 ⟶ ∀ x12 . x12 ∈ x6 ⟶ ∀ x13 . x13 ∈ x6 ⟶ ∀ x14 . x14 ∈ x6 ⟶ ∀ x15 . x15 ∈ x6 ⟶ x2 x4 x7 x8 x9 x10 x11 x12 x13 x14 x15 ⟶ 5bab1.. x3 x4) ⟶ ∀ x3 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x6) ⟶ 4402e.. x4 x5 ⟶ cf2df.. x4 x5 ⟶ ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ⊆ setminus x4 (Sing x6) ⟶ ∀ x8 . x8 ∈ x7 ⟶ ∀ x9 . x9 ∈ x7 ⟶ ∀ x10 . x10 ∈ x7 ⟶ ∀ x11 . x11 ∈ x7 ⟶ ∀ x12 . x12 ∈ x7 ⟶ ∀ x13 . x13 ∈ x7 ⟶ ∀ x14 . x14 ∈ x7 ⟶ ∀ x15 . x15 ∈ x7 ⟶ ∀ x16 . x16 ∈ x7 ⟶ x3 x5 x8 x9 x10 x11 x12 x13 x14 x15 x16 ⟶ 5bab1.. x4 x5) ⟶ ∀ x4 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x5 . ∀ x6 : ι → ι → ο . (∀ x7 . x7 ∈ x5 ⟶ ∀ x8 . x8 ∈ x5 ⟶ x6 x7 x8 ⟶ x6 x8 x7) ⟶ 4402e.. x5 x6 ⟶ cf2df.. x5 x6 ⟶ ∀ x7 . x7 ∈ x5 ⟶ ∀ x8 . x8 ⊆ setminus x5 (Sing x7) ⟶ ∀ x9 . x9 ∈ x8 ⟶ ∀ x10 . x10 ∈ x8 ⟶ ∀ x11 . x11 ∈ x8 ⟶ ∀ x12 . x12 ∈ x8 ⟶ ∀ x13 . x13 ∈ x8 ⟶ ∀ x14 . x14 ∈ x8 ⟶ ∀ x15 . x15 ∈ x8 ⟶ ∀ x16 . x16 ∈ x8 ⟶ ∀ x17 . x17 ∈ x8 ⟶ x4 x6 x9 x10 x11 x12 x13 x14 x15 x16 x17 ⟶ 5bab1.. x5 x6) ⟶ ∀ x5 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x6 . ∀ x7 : ι → ι → ο . (∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ x7 x8 x9 ⟶ x7 x9 x8) ⟶ 4402e.. x6 x7 ⟶ cf2df.. x6 x7 ⟶ ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ⊆ setminus x6 (Sing x8) ⟶ ∀ x10 . x10 ∈ x9 ⟶ ∀ x11 . x11 ∈ x9 ⟶ ∀ x12 . x12 ∈ x9 ⟶ ∀ x13 . x13 ∈ x9 ⟶ ∀ x14 . x14 ∈ x9 ⟶ ∀ x15 . x15 ∈ x9 ⟶ ∀ x16 . x16 ∈ x9 ⟶ ∀ x17 . x17 ∈ x9 ⟶ ∀ x18 . x18 ∈ x9 ⟶ x5 x7 x10 x11 x12 x13 x14 x15 x16 x17 x18 ⟶ 5bab1.. x6 x7) ⟶ ∀ x6 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x7 . ∀ x8 : ι → ι → ο . (∀ x9 . x9 ∈ x7 ⟶ ∀ x10 . x10 ∈ x7 ⟶ x8 x9 x10 ⟶ x8 x10 x9) ⟶ 4402e.. x7 x8 ⟶ cf2df.. x7 x8 ⟶ ∀ x9 . x9 ∈ x7 ⟶ ∀ x10 . x10 ⊆ setminus x7 (Sing x9) ⟶ ∀ x11 . x11 ∈ x10 ⟶ ∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ ∀ x14 . x14 ∈ x10 ⟶ ∀ x15 . x15 ∈ x10 ⟶ ∀ x16 . x16 ∈ x10 ⟶ ∀ x17 . x17 ∈ x10 ⟶ ∀ x18 . x18 ∈ x10 ⟶ ∀ x19 . x19 ∈ x10 ⟶ x6 x8 x11 x12 x13 x14 x15 x16 x17 x18 x19 ⟶ 5bab1.. x7 x8) ⟶ ∀ x7 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x8 . ∀ x9 : ι → ι → ο . (∀ x10 . x10 ∈ x8 ⟶ ∀ x11 . x11 ∈ x8 ⟶ x9 x10 x11 ⟶ x9 x11 x10) ⟶ 4402e.. x8 x9 ⟶ cf2df.. x8 x9 ⟶ ∀ x10 . x10 ∈ x8 ⟶ ∀ x11 . x11 ⊆ setminus x8 (Sing x10) ⟶ ∀ x12 . x12 ∈ x11 ⟶ ∀ x13 . x13 ∈ x11 ⟶ ∀ x14 . x14 ∈ x11 ⟶ ∀ x15 . x15 ∈ x11 ⟶ ∀ x16 . x16 ∈ x11 ⟶ ∀ x17 . x17 ∈ x11 ⟶ ∀ x18 . x18 ∈ x11 ⟶ ∀ x19 . x19 ∈ x11 ⟶ ∀ x20 . x20 ∈ x11 ⟶ x7 x9 x12 x13 x14 x15 x16 x17 x18 x19 x20 ⟶ 5bab1.. x8 x9) ⟶ ∀ x8 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x9 . ∀ x10 : ι → ι → ο . (∀ x11 . x11 ∈ x9 ⟶ ∀ x12 . x12 ∈ x9 ⟶ x10 x11 x12 ⟶ x10 x12 x11) ⟶ 4402e.. x9 x10 ⟶ cf2df.. x9 x10 ⟶ ∀ x11 . x11 ∈ x9 ⟶ ∀ x12 . x12 ⊆ setminus x9 (Sing x11) ⟶ ∀ x13 . x13 ∈ x12 ⟶ ∀ x14 . x14 ∈ x12 ⟶ ∀ x15 . x15 ∈ x12 ⟶ ∀ x16 . x16 ∈ x12 ⟶ ∀ x17 . x17 ∈ x12 ⟶ ∀ x18 . x18 ∈ x12 ⟶ ∀ x19 . x19 ∈ x12 ⟶ ∀ x20 . x20 ∈ x12 ⟶ ∀ x21 . x21 ∈ x12 ⟶ x8 x10 x13 x14 x15 x16 x17 x18 x19 x20 x21 ⟶ 5bab1.. x9 x10) ⟶ ∀ x9 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x10 . ∀ x11 : ι → ι → ο . (∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ∈ x10 ⟶ x11 x12 x13 ⟶ x11 x13 x12) ⟶ 4402e.. x10 x11 ⟶ cf2df.. x10 x11 ⟶ ∀ x12 . x12 ∈ x10 ⟶ ∀ x13 . x13 ⊆ setminus x10 (Sing x12) ⟶ ∀ x14 . x14 ∈ x13 ⟶ ∀ x15 . x15 ∈ x13 ⟶ ∀ x16 . x16 ∈ x13 ⟶ ∀ x17 . x17 ∈ x13 ⟶ ∀ x18 . x18 ∈ x13 ⟶ ∀ x19 . x19 ∈ x13 ⟶ ∀ x20 . x20 ∈ x13 ⟶ ∀ x21 . x21 ∈ x13 ⟶ ∀ x22 . x22 ∈ x13 ⟶ x9 x11 x14 x15 x16 x17 x18 x19 x20 x21 x22 ⟶ 5bab1.. x10 x11) ⟶ ∀ x10 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x11 . ∀ x12 : ι → ι → ο . (∀ x13 . x13 ∈ x11 ⟶ ∀ x14 . x14 ∈ x11 ⟶ x12 x13 x14 ⟶ x12 x14 x13) ⟶ 4402e.. x11 x12 ⟶ cf2df.. x11 x12 ⟶ ∀ x13 . x13 ∈ x11 ⟶ ∀ x14 . x14 ⊆ setminus x11 (Sing x13) ⟶ ∀ x15 . x15 ∈ x14 ⟶ ∀ x16 . x16 ∈ x14 ⟶ ∀ x17 . x17 ∈ x14 ⟶ ∀ x18 . x18 ∈ x14 ⟶ ∀ x19 . x19 ∈ x14 ⟶ ∀ x20 . x20 ∈ x14 ⟶ ∀ x21 . x21 ∈ x14 ⟶ ∀ x22 . x22 ∈ x14 ⟶ ∀ x23 . x23 ∈ x14 ⟶ x10 x12 x15 x16 x17 x18 x19 x20 x21 x22 x23 ⟶ 5bab1.. x11 x12) ⟶ ∀ x11 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x12 . ∀ x13 : ι → ι → ο . (∀ x14 . x14 ∈ x12 ⟶ ∀ x15 . x15 ∈ x12 ⟶ x13 x14 x15 ⟶ x13 x15 x14) ⟶ 4402e.. x12 x13 ⟶ cf2df.. x12 x13 ⟶ ∀ x14 . x14 ∈ x12 ⟶ ∀ x15 . x15 ⊆ setminus x12 (Sing x14) ⟶ ∀ x16 . x16 ∈ x15 ⟶ ∀ x17 . x17 ∈ x15 ⟶ ∀ x18 . x18 ∈ x15 ⟶ ∀ x19 . x19 ∈ x15 ⟶ ∀ x20 . x20 ∈ x15 ⟶ ∀ x21 . x21 ∈ x15 ⟶ ∀ x22 . x22 ∈ x15 ⟶ ∀ x23 . x23 ∈ x15 ⟶ ∀ x24 . x24 ∈ x15 ⟶ x11 x13 x16 x17 x18 x19 x20 x21 x22 x23 x24 ⟶ 5bab1.. x12 x13) ⟶ ∀ x12 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x13 . ∀ x14 : ι → ι → ο . (∀ x15 . x15 ∈ x13 ⟶ ∀ x16 . x16 ∈ x13 ⟶ x14 x15 x16 ⟶ x14 x16 x15) ⟶ 4402e.. x13 x14 ⟶ cf2df.. x13 x14 ⟶ ∀ x15 . x15 ∈ x13 ⟶ ∀ x16 . x16 ⊆ setminus x13 (Sing x15) ⟶ ∀ x17 . x17 ∈ x16 ⟶ ∀ x18 . x18 ∈ x16 ⟶ ∀ x19 . x19 ∈ x16 ⟶ ∀ x20 . x20 ∈ x16 ⟶ ∀ x21 . x21 ∈ x16 ⟶ ∀ x22 . x22 ∈ x16 ⟶ ∀ x23 . x23 ∈ x16 ⟶ ∀ x24 . x24 ∈ x16 ⟶ ∀ x25 . x25 ∈ x16 ⟶ x12 x14 x17 x18 x19 x20 x21 x22 x23 x24 x25 ⟶ 5bab1.. x13 x14) ⟶ ∀ x13 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x14 . ∀ x15 : ι → ι → ο . (∀ x16 . x16 ∈ x14 ⟶ ∀ x17 . x17 ∈ x14 ⟶ x15 x16 x17 ⟶ x15 x17 x16) ⟶ 4402e.. x14 x15 ⟶ cf2df.. x14 x15 ⟶ ∀ x16 . x16 ∈ x14 ⟶ ∀ x17 . x17 ⊆ setminus x14 (Sing x16) ⟶ ∀ x18 . x18 ∈ x17 ⟶ ∀ x19 . x19 ∈ x17 ⟶ ∀ x20 . x20 ∈ x17 ⟶ ∀ x21 . x21 ∈ x17 ⟶ ∀ x22 . x22 ∈ x17 ⟶ ∀ x23 . x23 ∈ x17 ⟶ ∀ x24 . x24 ∈ x17 ⟶ ∀ x25 . x25 ∈ x17 ⟶ ∀ x26 . x26 ∈ x17 ⟶ x13 x15 x18 x19 x20 x21 x22 x23 x24 x25 x26 ⟶ 5bab1.. x14 x15) ⟶ ∀ x14 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x15 . ∀ x16 : ι → ι → ο . (∀ x17 . x17 ∈ x15 ⟶ ∀ x18 . x18 ∈ x15 ⟶ x16 x17 x18 ⟶ x16 x18 x17) ⟶ 4402e.. x15 x16 ⟶ cf2df.. x15 x16 ⟶ ∀ x17 . x17 ∈ x15 ⟶ ∀ x18 . x18 ⊆ setminus x15 (Sing x17) ⟶ ∀ x19 . x19 ∈ x18 ⟶ ∀ x20 . x20 ∈ x18 ⟶ ∀ x21 . x21 ∈ x18 ⟶ ∀ x22 . x22 ∈ x18 ⟶ ∀ x23 . x23 ∈ x18 ⟶ ∀ x24 . x24 ∈ x18 ⟶ ∀ x25 . x25 ∈ x18 ⟶ ∀ x26 . x26 ∈ x18 ⟶ ∀ x27 . x27 ∈ x18 ⟶ x14 x16 x19 x20 x21 x22 x23 x24 x25 x26 x27 ⟶ 5bab1.. x15 x16) ⟶ ∀ x15 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x16 . ∀ x17 : ι → ι → ο . (∀ x18 . x18 ∈ x16 ⟶ ∀ x19 . x19 ∈ x16 ⟶ x17 x18 x19 ⟶ x17 x19 x18) ⟶ 4402e.. x16 x17 ⟶ cf2df.. x16 x17 ⟶ ∀ x18 . x18 ∈ x16 ⟶ ∀ x19 . x19 ⊆ setminus x16 (Sing x18) ⟶ ∀ x20 . x20 ∈ x19 ⟶ ∀ x21 . x21 ∈ x19 ⟶ ∀ x22 . x22 ∈ x19 ⟶ ∀ x23 . x23 ∈ x19 ⟶ ∀ x24 . x24 ∈ x19 ⟶ ∀ x25 . x25 ∈ x19 ⟶ ∀ x26 . x26 ∈ x19 ⟶ ∀ x27 . x27 ∈ x19 ⟶ ∀ x28 . x28 ∈ x19 ⟶ x15 x17 x20 x21 x22 x23 x24 x25 x26 x27 x28 ⟶ 5bab1.. x16 x17) ⟶ ∀ x16 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x17 . ∀ x18 : ι → ι → ο . (∀ x19 . x19 ∈ x17 ⟶ ∀ x20 . x20 ∈ x17 ⟶ x18 x19 x20 ⟶ x18 x20 x19) ⟶ 4402e.. x17 x18 ⟶ cf2df.. x17 x18 ⟶ ∀ x19 . x19 ∈ x17 ⟶ ∀ x20 . x20 ⊆ setminus x17 (Sing x19) ⟶ ∀ x21 . x21 ∈ x20 ⟶ ∀ x22 . x22 ∈ x20 ⟶ ∀ x23 . x23 ∈ x20 ⟶ ∀ x24 . x24 ∈ x20 ⟶ ∀ x25 . x25 ∈ x20 ⟶ ∀ x26 . x26 ∈ x20 ⟶ ∀ x27 . x27 ∈ x20 ⟶ ∀ x28 . x28 ∈ x20 ⟶ ∀ x29 . x29 ∈ x20 ⟶ x16 x18 x21 x22 x23 x24 x25 x26 x27 x28 x29 ⟶ 5bab1.. x17 x18) ⟶ ∀ x17 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x18 . ∀ x19 : ι → ι → ο . (∀ x20 . x20 ∈ x18 ⟶ ∀ x21 . x21 ∈ x18 ⟶ x19 x20 x21 ⟶ x19 x21 x20) ⟶ 4402e.. x18 x19 ⟶ cf2df.. x18 x19 ⟶ ∀ x20 . x20 ∈ x18 ⟶ ∀ x21 . x21 ⊆ setminus x18 (Sing x20) ⟶ ∀ x22 . x22 ∈ x21 ⟶ ∀ x23 . x23 ∈ x21 ⟶ ∀ x24 . x24 ∈ x21 ⟶ ∀ x25 . x25 ∈ x21 ⟶ ∀ x26 . x26 ∈ x21 ⟶ ∀ x27 . x27 ∈ x21 ⟶ ∀ x28 . x28 ∈ x21 ⟶ ∀ x29 . x29 ∈ x21 ⟶ ∀ x30 . x30 ∈ x21 ⟶ x17 x19 x22 x23 x24 x25 x26 x27 x28 x29 x30 ⟶ 5bab1.. x18 x19) ⟶ ∀ x18 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x19 . ∀ x20 : ι → ι → ο . (∀ x21 . x21 ∈ x19 ⟶ ∀ x22 . x22 ∈ x19 ⟶ x20 x21 x22 ⟶ x20 x22 x21) ⟶ 4402e.. x19 x20 ⟶ cf2df.. x19 x20 ⟶ ∀ x21 . x21 ∈ x19 ⟶ ∀ x22 . x22 ⊆ setminus x19 (Sing x21) ⟶ ∀ x23 . x23 ∈ x22 ⟶ ∀ x24 . x24 ∈ x22 ⟶ ∀ x25 . x25 ∈ x22 ⟶ ∀ x26 . x26 ∈ x22 ⟶ ∀ x27 . x27 ∈ x22 ⟶ ∀ x28 . x28 ∈ x22 ⟶ ∀ x29 . x29 ∈ x22 ⟶ ∀ x30 . x30 ∈ x22 ⟶ ∀ x31 . x31 ∈ x22 ⟶ x18 x20 x23 x24 x25 x26 x27 x28 x29 x30 x31 ⟶ 5bab1.. x19 x20) ⟶ ∀ x19 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x20 . ∀ x21 : ι → ι → ο . (∀ x22 . x22 ∈ x20 ⟶ ∀ x23 . x23 ∈ x20 ⟶ x21 x22 x23 ⟶ x21 x23 x22) ⟶ 4402e.. x20 x21 ⟶ cf2df.. x20 x21 ⟶ ∀ x22 . x22 ∈ x20 ⟶ ∀ x23 . x23 ⊆ setminus x20 (Sing x22) ⟶ ∀ x24 . x24 ∈ x23 ⟶ ∀ x25 . x25 ∈ x23 ⟶ ∀ x26 . x26 ∈ x23 ⟶ ∀ x27 . x27 ∈ x23 ⟶ ∀ x28 . x28 ∈ x23 ⟶ ∀ x29 . x29 ∈ x23 ⟶ ∀ x30 . x30 ∈ x23 ⟶ ∀ x31 . x31 ∈ x23 ⟶ ∀ x32 . x32 ∈ x23 ⟶ x19 x21 x24 x25 x26 x27 x28 x29 x30 x31 x32 ⟶ 5bab1.. x20 x21) ⟶ ∀ x20 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x21 . ∀ x22 : ι → ι → ο . (∀ x23 . x23 ∈ x21 ⟶ ∀ x24 . x24 ∈ x21 ⟶ x22 x23 x24 ⟶ x22 x24 x23) ⟶ 4402e.. x21 x22 ⟶ cf2df.. x21 x22 ⟶ ∀ x23 . x23 ∈ x21 ⟶ ∀ x24 . x24 ⊆ setminus x21 (Sing x23) ⟶ ∀ x25 . x25 ∈ x24 ⟶ ∀ x26 . x26 ∈ x24 ⟶ ∀ x27 . x27 ∈ x24 ⟶ ∀ x28 . x28 ∈ x24 ⟶ ∀ x29 . x29 ∈ x24 ⟶ ∀ x30 . x30 ∈ x24 ⟶ ∀ x31 . x31 ∈ x24 ⟶ ∀ x32 . x32 ∈ x24 ⟶ ∀ x33 . x33 ∈ x24 ⟶ x20 x22 x25 x26 x27 x28 x29 x30 x31 x32 x33 ⟶ 5bab1.. x21 x22) ⟶ ∀ x21 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x22 . ∀ x23 : ι → ι → ο . (∀ x24 . x24 ∈ x22 ⟶ ∀ x25 . x25 ∈ x22 ⟶ x23 x24 x25 ⟶ x23 x25 x24) ⟶ 4402e.. x22 x23 ⟶ cf2df.. x22 x23 ⟶ ∀ x24 . x24 ∈ x22 ⟶ ∀ x25 . x25 ⊆ setminus x22 (Sing x24) ⟶ ∀ x26 . x26 ∈ x25 ⟶ ∀ x27 . x27 ∈ x25 ⟶ ∀ x28 . x28 ∈ x25 ⟶ ∀ x29 . x29 ∈ x25 ⟶ ∀ x30 . x30 ∈ x25 ⟶ ∀ x31 . x31 ∈ x25 ⟶ ∀ x32 . x32 ∈ x25 ⟶ ∀ x33 . x33 ∈ x25 ⟶ ∀ x34 . x34 ∈ x25 ⟶ x21 x23 x26 x27 x28 x29 x30 x31 x32 x33 x34 ⟶ 5bab1.. x22 x23) ⟶ ∀ x22 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x23 . ∀ x24 : ι → ι → ο . (∀ x25 . x25 ∈ x23 ⟶ ∀ x26 . x26 ∈ x23 ⟶ x24 x25 x26 ⟶ x24 x26 x25) ⟶ 4402e.. x23 x24 ⟶ cf2df.. x23 x24 ⟶ ∀ x25 . x25 ∈ x23 ⟶ ∀ x26 . x26 ⊆ setminus x23 (Sing x25) ⟶ ∀ x27 . x27 ∈ x26 ⟶ ∀ x28 . x28 ∈ x26 ⟶ ∀ x29 . x29 ∈ x26 ⟶ ∀ x30 . x30 ∈ x26 ⟶ ∀ x31 . x31 ∈ x26 ⟶ ∀ x32 . x32 ∈ x26 ⟶ ∀ x33 . x33 ∈ x26 ⟶ ∀ x34 . x34 ∈ x26 ⟶ ∀ x35 . x35 ∈ x26 ⟶ x22 x24 x27 x28 x29 x30 x31 x32 x33 x34 x35 ⟶ 5bab1.. x23 x24) ⟶ ∀ x23 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x24 . ∀ x25 : ι → ι → ο . (∀ x26 . x26 ∈ x24 ⟶ ∀ x27 . x27 ∈ x24 ⟶ x25 x26 x27 ⟶ x25 x27 x26) ⟶ 4402e.. x24 x25 ⟶ cf2df.. x24 x25 ⟶ ∀ x26 . x26 ∈ x24 ⟶ ∀ x27 . x27 ⊆ setminus x24 (Sing x26) ⟶ ∀ x28 . x28 ∈ x27 ⟶ ∀ x29 . x29 ∈ x27 ⟶ ∀ x30 . x30 ∈ x27 ⟶ ∀ x31 . x31 ∈ x27 ⟶ ∀ x32 . x32 ∈ x27 ⟶ ∀ x33 . x33 ∈ x27 ⟶ ∀ x34 . x34 ∈ x27 ⟶ ∀ x35 . x35 ∈ x27 ⟶ ∀ x36 . x36 ∈ x27 ⟶ x23 x25 x28 x29 x30 x31 x32 x33 x34 x35 x36 ⟶ 5bab1.. x24 x25) ⟶ ∀ x24 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x25 . ∀ x26 : ι → ι → ο . (∀ x27 . x27 ∈ x25 ⟶ ∀ x28 . x28 ∈ x25 ⟶ x26 x27 x28 ⟶ x26 x28 x27) ⟶ 4402e.. x25 x26 ⟶ cf2df.. x25 x26 ⟶ ∀ x27 . x27 ∈ x25 ⟶ ∀ x28 . x28 ⊆ setminus x25 (Sing x27) ⟶ ∀ x29 . x29 ∈ x28 ⟶ ∀ x30 . x30 ∈ x28 ⟶ ∀ x31 . x31 ∈ x28 ⟶ ∀ x32 . x32 ∈ x28 ⟶ ∀ x33 . x33 ∈ x28 ⟶ ∀ x34 . x34 ∈ x28 ⟶ ∀ x35 . x35 ∈ x28 ⟶ ∀ x36 . x36 ∈ x28 ⟶ ∀ x37 . x37 ∈ x28 ⟶ x24 x26 x29 x30 x31 x32 x33 x34 x35 x36 x37 ⟶ 5bab1.. x25 x26) ⟶ ∀ x25 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x26 . ∀ x27 : ι → ι → ο . (∀ x28 . x28 ∈ x26 ⟶ ∀ x29 . x29 ∈ x26 ⟶ x27 x28 x29 ⟶ x27 x29 x28) ⟶ 4402e.. x26 x27 ⟶ cf2df.. x26 x27 ⟶ ∀ x28 . x28 ∈ x26 ⟶ ∀ x29 . x29 ⊆ setminus x26 (Sing x28) ⟶ ∀ x30 . x30 ∈ x29 ⟶ ∀ x31 . x31 ∈ x29 ⟶ ∀ x32 . x32 ∈ x29 ⟶ ∀ x33 . x33 ∈ x29 ⟶ ∀ x34 . x34 ∈ x29 ⟶ ∀ x35 . x35 ∈ x29 ⟶ ∀ x36 . x36 ∈ x29 ⟶ ∀ x37 . x37 ∈ x29 ⟶ ∀ x38 . x38 ∈ x29 ⟶ x25 x27 x30 x31 x32 x33 x34 x35 x36 x37 x38 ⟶ 5bab1.. x26 x27) ⟶ ∀ x26 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x27 . ∀ x28 : ι → ι → ο . (∀ x29 . x29 ∈ x27 ⟶ ∀ x30 . x30 ∈ x27 ⟶ x28 x29 x30 ⟶ x28 x30 x29) ⟶ 4402e.. x27 x28 ⟶ cf2df.. x27 x28 ⟶ ∀ x29 . x29 ∈ x27 ⟶ ∀ x30 . x30 ⊆ setminus x27 (Sing x29) ⟶ ∀ x31 . x31 ∈ x30 ⟶ ∀ x32 . x32 ∈ x30 ⟶ ∀ x33 . x33 ∈ x30 ⟶ ∀ x34 . x34 ∈ x30 ⟶ ∀ x35 . x35 ∈ x30 ⟶ ∀ x36 . x36 ∈ x30 ⟶ ∀ x37 . x37 ∈ x30 ⟶ ∀ x38 . x38 ∈ x30 ⟶ ∀ x39 . x39 ∈ x30 ⟶ x26 x28 x31 x32 x33 x34 x35 x36 x37 x38 x39 ⟶ 5bab1.. x27 x28) ⟶ ∀ x27 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x28 . ∀ x29 : ι → ι → ο . (∀ x30 . x30 ∈ x28 ⟶ ∀ x31 . x31 ∈ x28 ⟶ x29 x30 x31 ⟶ x29 x31 x30) ⟶ 4402e.. x28 x29 ⟶ cf2df.. x28 x29 ⟶ ∀ x30 . x30 ∈ x28 ⟶ ∀ x31 . x31 ⊆ setminus x28 (Sing x30) ⟶ ∀ x32 . x32 ∈ x31 ⟶ ∀ x33 . x33 ∈ x31 ⟶ ∀ x34 . x34 ∈ x31 ⟶ ∀ x35 . x35 ∈ x31 ⟶ ∀ x36 . x36 ∈ x31 ⟶ ∀ x37 . x37 ∈ x31 ⟶ ∀ x38 . x38 ∈ x31 ⟶ ∀ x39 . x39 ∈ x31 ⟶ ∀ x40 . x40 ∈ x31 ⟶ x27 x29 x32 x33 x34 x35 x36 x37 x38 x39 x40 ⟶ 5bab1.. x28 x29) ⟶ ∀ x28 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x29 . ∀ x30 : ι → ι → ο . (∀ x31 . x31 ∈ x29 ⟶ ∀ x32 . x32 ∈ x29 ⟶ x30 x31 x32 ⟶ x30 x32 x31) ⟶ 4402e.. x29 x30 ⟶ cf2df.. x29 x30 ⟶ ∀ x31 . x31 ∈ x29 ⟶ ∀ x32 . x32 ⊆ setminus x29 (Sing x31) ⟶ ∀ x33 . x33 ∈ x32 ⟶ ∀ x34 . x34 ∈ x32 ⟶ ∀ x35 . x35 ∈ x32 ⟶ ∀ x36 . x36 ∈ x32 ⟶ ∀ x37 . x37 ∈ x32 ⟶ ∀ x38 . x38 ∈ x32 ⟶ ∀ x39 . x39 ∈ x32 ⟶ ∀ x40 . x40 ∈ x32 ⟶ ∀ x41 . x41 ∈ x32 ⟶ x28 x30 x33 x34 x35 x36 x37 x38 x39 x40 x41 ⟶ 5bab1.. x29 x30) ⟶ ∀ x29 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x30 . ∀ x31 : ι → ι → ο . (∀ x32 . x32 ∈ x30 ⟶ ∀ x33 . x33 ∈ x30 ⟶ x31 x32 x33 ⟶ x31 x33 x32) ⟶ 4402e.. x30 x31 ⟶ cf2df.. x30 x31 ⟶ ∀ x32 . x32 ∈ x30 ⟶ ∀ x33 . x33 ⊆ setminus x30 (Sing x32) ⟶ ∀ x34 . x34 ∈ x33 ⟶ ∀ x35 . x35 ∈ x33 ⟶ ∀ x36 . x36 ∈ x33 ⟶ ∀ x37 . x37 ∈ x33 ⟶ ∀ x38 . x38 ∈ x33 ⟶ ∀ x39 . x39 ∈ x33 ⟶ ∀ x40 . x40 ∈ x33 ⟶ ∀ x41 . x41 ∈ x33 ⟶ ∀ x42 . x42 ∈ x33 ⟶ x29 x31 x34 x35 x36 x37 x38 x39 x40 x41 x42 ⟶ 5bab1.. x30 x31) ⟶ ∀ x30 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x31 . ∀ x32 : ι → ι → ο . (∀ x33 . x33 ∈ x31 ⟶ ∀ x34 . x34 ∈ x31 ⟶ x32 x33 x34 ⟶ x32 x34 x33) ⟶ 4402e.. x31 x32 ⟶ cf2df.. x31 x32 ⟶ ∀ x33 . x33 ∈ x31 ⟶ ∀ x34 . x34 ⊆ setminus x31 (Sing x33) ⟶ ∀ x35 . x35 ∈ x34 ⟶ ∀ x36 . x36 ∈ x34 ⟶ ∀ x37 . x37 ∈ x34 ⟶ ∀ x38 . x38 ∈ x34 ⟶ ∀ x39 . x39 ∈ x34 ⟶ ∀ x40 . x40 ∈ x34 ⟶ ∀ x41 . x41 ∈ x34 ⟶ ∀ x42 . x42 ∈ x34 ⟶ ∀ x43 . x43 ∈ x34 ⟶ x30 x32 x35 x36 x37 x38 x39 x40 x41 x42 x43 ⟶ 5bab1.. x31 x32) ⟶ ∀ x31 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x32 . ∀ x33 : ι → ι → ο . (∀ x34 . x34 ∈ x32 ⟶ ∀ x35 . x35 ∈ x32 ⟶ x33 x34 x35 ⟶ x33 x35 x34) ⟶ 4402e.. x32 x33 ⟶ cf2df.. x32 x33 ⟶ ∀ x34 . x34 ∈ x32 ⟶ ∀ x35 . x35 ⊆ setminus x32 (Sing x34) ⟶ ∀ x36 . x36 ∈ x35 ⟶ ∀ x37 . x37 ∈ x35 ⟶ ∀ x38 . x38 ∈ x35 ⟶ ∀ x39 . x39 ∈ x35 ⟶ ∀ x40 . x40 ∈ x35 ⟶ ∀ x41 . x41 ∈ x35 ⟶ ∀ x42 . x42 ∈ x35 ⟶ ∀ x43 . x43 ∈ x35 ⟶ ∀ x44 . x44 ∈ x35 ⟶ x31 x33 x36 x37 x38 x39 x40 x41 x42 x43 x44 ⟶ 5bab1.. x32 x33) ⟶ ∀ x32 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x33 . ∀ x34 : ι → ι → ο . (∀ x35 . x35 ∈ x33 ⟶ ∀ x36 . x36 ∈ x33 ⟶ x34 x35 x36 ⟶ x34 x36 x35) ⟶ 4402e.. x33 x34 ⟶ cf2df.. x33 x34 ⟶ ∀ x35 . x35 ∈ x33 ⟶ ∀ x36 . x36 ⊆ setminus x33 (Sing x35) ⟶ ∀ x37 . x37 ∈ x36 ⟶ ∀ x38 . x38 ∈ x36 ⟶ ∀ x39 . x39 ∈ x36 ⟶ ∀ x40 . x40 ∈ x36 ⟶ ∀ x41 . x41 ∈ x36 ⟶ ∀ x42 . x42 ∈ x36 ⟶ ∀ x43 . x43 ∈ x36 ⟶ ∀ x44 . x44 ∈ x36 ⟶ ∀ x45 . x45 ∈ x36 ⟶ x32 x34 x37 x38 x39 x40 x41 x42 x43 x44 x45 ⟶ 5bab1.. x33 x34) ⟶ ∀ x33 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x34 . ∀ x35 : ι → ι → ο . (∀ x36 . x36 ∈ x34 ⟶ ∀ x37 . x37 ∈ x34 ⟶ x35 x36 x37 ⟶ x35 x37 x36) ⟶ 4402e.. x34 x35 ⟶ cf2df.. x34 x35 ⟶ ∀ x36 . x36 ∈ x34 ⟶ ∀ x37 . x37 ⊆ setminus x34 (Sing x36) ⟶ ∀ x38 . x38 ∈ x37 ⟶ ∀ x39 . x39 ∈ x37 ⟶ ∀ x40 . x40 ∈ x37 ⟶ ∀ x41 . x41 ∈ x37 ⟶ ∀ x42 . x42 ∈ x37 ⟶ ∀ x43 . x43 ∈ x37 ⟶ ∀ x44 . x44 ∈ x37 ⟶ ∀ x45 . x45 ∈ x37 ⟶ ∀ x46 . x46 ∈ x37 ⟶ x33 x35 x38 x39 x40 x41 x42 x43 x44 x45 x46 ⟶ 5bab1.. x34 x35) ⟶ ∀ x34 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x35 . ∀ x36 : ι → ι → ο . (∀ x37 . x37 ∈ x35 ⟶ ∀ x38 . x38 ∈ x35 ⟶ x36 x37 x38 ⟶ x36 x38 x37) ⟶ 4402e.. x35 x36 ⟶ cf2df.. x35 x36 ⟶ ∀ x37 . x37 ∈ x35 ⟶ ∀ x38 . x38 ⊆ setminus x35 (Sing x37) ⟶ ∀ x39 . x39 ∈ x38 ⟶ ∀ x40 . x40 ∈ x38 ⟶ ∀ x41 . x41 ∈ x38 ⟶ ∀ x42 . x42 ∈ x38 ⟶ ∀ x43 . x43 ∈ x38 ⟶ ∀ x44 . x44 ∈ x38 ⟶ ∀ x45 . x45 ∈ x38 ⟶ ∀ x46 . x46 ∈ x38 ⟶ ∀ x47 . x47 ∈ x38 ⟶ x34 x36 x39 x40 x41 x42 x43 x44 x45 x46 x47 ⟶ 5bab1.. x35 x36) ⟶ ∀ x35 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x36 . ∀ x37 : ι → ι → ο . (∀ x38 . x38 ∈ x36 ⟶ ∀ x39 . x39 ∈ x36 ⟶ x37 x38 x39 ⟶ x37 x39 x38) ⟶ 4402e.. x36 x37 ⟶ cf2df.. x36 x37 ⟶ ∀ x38 . x38 ∈ x36 ⟶ ∀ x39 . x39 ⊆ setminus x36 (Sing x38) ⟶ ∀ x40 . x40 ∈ x39 ⟶ ∀ x41 . x41 ∈ x39 ⟶ ∀ x42 . x42 ∈ x39 ⟶ ∀ x43 . x43 ∈ x39 ⟶ ∀ x44 . x44 ∈ x39 ⟶ ∀ x45 . x45 ∈ x39 ⟶ ∀ x46 . x46 ∈ x39 ⟶ ∀ x47 . x47 ∈ x39 ⟶ ∀ x48 . x48 ∈ x39 ⟶ x35 x37 x40 x41 x42 x43 x44 x45 x46 x47 x48 ⟶ 5bab1.. x36 x37) ⟶ ∀ x36 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x37 . ∀ x38 : ι → ι → ο . (∀ x39 . x39 ∈ x37 ⟶ ∀ x40 . x40 ∈ x37 ⟶ x38 x39 x40 ⟶ x38 x40 x39) ⟶ 4402e.. x37 x38 ⟶ cf2df.. x37 x38 ⟶ ∀ x39 . x39 ∈ x37 ⟶ ∀ x40 . x40 ⊆ setminus x37 (Sing x39) ⟶ ∀ x41 . x41 ∈ x40 ⟶ ∀ x42 . x42 ∈ x40 ⟶ ∀ x43 . x43 ∈ x40 ⟶ ∀ x44 . x44 ∈ x40 ⟶ ∀ x45 . x45 ∈ x40 ⟶ ∀ x46 . x46 ∈ x40 ⟶ ∀ x47 . x47 ∈ x40 ⟶ ∀ x48 . x48 ∈ x40 ⟶ ∀ x49 . x49 ∈ x40 ⟶ x36 x38 x41 x42 x43 x44 x45 x46 x47 x48 x49 ⟶ 5bab1.. x37 x38) ⟶ ∀ x37 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x38 . ∀ x39 : ι → ι → ο . (∀ x40 . x40 ∈ x38 ⟶ ∀ x41 . x41 ∈ x38 ⟶ x39 x40 x41 ⟶ x39 x41 x40) ⟶ 4402e.. x38 x39 ⟶ cf2df.. x38 x39 ⟶ ∀ x40 . x40 ∈ x38 ⟶ ∀ x41 . x41 ⊆ setminus x38 (Sing x40) ⟶ ∀ x42 . x42 ∈ x41 ⟶ ∀ x43 . x43 ∈ x41 ⟶ ∀ x44 . x44 ∈ x41 ⟶ ∀ x45 . x45 ∈ x41 ⟶ ∀ x46 . x46 ∈ x41 ⟶ ∀ x47 . x47 ∈ x41 ⟶ ∀ x48 . x48 ∈ x41 ⟶ ∀ x49 . x49 ∈ x41 ⟶ ∀ x50 . x50 ∈ x41 ⟶ x37 x39 x42 x43 x44 x45 x46 x47 x48 x49 x50 ⟶ 5bab1.. x38 x39) ⟶ ∀ x38 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x39 . ∀ x40 : ι → ι → ο . (∀ x41 . x41 ∈ x39 ⟶ ∀ x42 . x42 ∈ x39 ⟶ x40 x41 x42 ⟶ x40 x42 x41) ⟶ 4402e.. x39 x40 ⟶ cf2df.. x39 x40 ⟶ ∀ x41 . x41 ∈ x39 ⟶ ∀ x42 . x42 ⊆ setminus x39 (Sing x41) ⟶ ∀ x43 . x43 ∈ x42 ⟶ ∀ x44 . x44 ∈ x42 ⟶ ∀ x45 . x45 ∈ x42 ⟶ ∀ x46 . x46 ∈ x42 ⟶ ∀ x47 . x47 ∈ x42 ⟶ ∀ x48 . x48 ∈ x42 ⟶ ∀ x49 . x49 ∈ x42 ⟶ ∀ x50 . x50 ∈ x42 ⟶ ∀ x51 . x51 ∈ x42 ⟶ x38 x40 x43 x44 x45 x46 x47 x48 x49 x50 x51 ⟶ 5bab1.. x39 x40) ⟶ ∀ x39 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x40 . ∀ x41 : ι → ι → ο . (∀ x42 . x42 ∈ x40 ⟶ ∀ x43 . x43 ∈ x40 ⟶ x41 x42 x43 ⟶ x41 x43 x42) ⟶ 4402e.. x40 x41 ⟶ cf2df.. x40 x41 ⟶ ∀ x42 . x42 ∈ x40 ⟶ ∀ x43 . x43 ⊆ setminus x40 (Sing x42) ⟶ ∀ x44 . x44 ∈ x43 ⟶ ∀ x45 . x45 ∈ x43 ⟶ ∀ x46 . x46 ∈ x43 ⟶ ∀ x47 . x47 ∈ x43 ⟶ ∀ x48 . x48 ∈ x43 ⟶ ∀ x49 . x49 ∈ x43 ⟶ ∀ x50 . x50 ∈ x43 ⟶ ∀ x51 . x51 ∈ x43 ⟶ ∀ x52 . x52 ∈ x43 ⟶ x39 x41 x44 x45 x46 x47 x48 x49 x50 x51 x52 ⟶ 5bab1.. x40 x41) ⟶ ∀ x40 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x41 . ∀ x42 : ι → ι → ο . (∀ x43 . x43 ∈ x41 ⟶ ∀ x44 . x44 ∈ x41 ⟶ x42 x43 x44 ⟶ x42 x44 x43) ⟶ 4402e.. x41 x42 ⟶ cf2df.. x41 x42 ⟶ ∀ x43 . x43 ∈ x41 ⟶ ∀ x44 . x44 ⊆ setminus x41 (Sing x43) ⟶ ∀ x45 . x45 ∈ x44 ⟶ ∀ x46 . x46 ∈ x44 ⟶ ∀ x47 . x47 ∈ x44 ⟶ ∀ x48 . x48 ∈ x44 ⟶ ∀ x49 . x49 ∈ x44 ⟶ ∀ x50 . x50 ∈ x44 ⟶ ∀ x51 . x51 ∈ x44 ⟶ ∀ x52 . x52 ∈ x44 ⟶ ∀ x53 . x53 ∈ x44 ⟶ x40 x42 x45 x46 x47 x48 x49 x50 x51 x52 x53 ⟶ 5bab1.. x41 x42) ⟶ ∀ x41 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x42 . ∀ x43 : ι → ι → ο . (∀ x44 . x44 ∈ x42 ⟶ ∀ x45 . x45 ∈ x42 ⟶ x43 x44 x45 ⟶ x43 x45 x44) ⟶ 4402e.. x42 x43 ⟶ cf2df.. x42 x43 ⟶ ∀ x44 . x44 ∈ x42 ⟶ ∀ x45 . x45 ⊆ setminus x42 (Sing x44) ⟶ ∀ x46 . x46 ∈ x45 ⟶ ∀ x47 . x47 ∈ x45 ⟶ ∀ x48 . x48 ∈ x45 ⟶ ∀ x49 . x49 ∈ x45 ⟶ ∀ x50 . x50 ∈ x45 ⟶ ∀ x51 . x51 ∈ x45 ⟶ ∀ x52 . x52 ∈ x45 ⟶ ∀ x53 . x53 ∈ x45 ⟶ ∀ x54 . x54 ∈ x45 ⟶ x41 x43 x46 x47 x48 x49 x50 x51 x52 x53 x54 ⟶ 5bab1.. x42 x43) ⟶ ∀ x42 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x43 . ∀ x44 : ι → ι → ο . (∀ x45 . x45 ∈ x43 ⟶ ∀ x46 . x46 ∈ x43 ⟶ x44 x45 x46 ⟶ x44 x46 x45) ⟶ 4402e.. x43 x44 ⟶ cf2df.. x43 x44 ⟶ ∀ x45 . x45 ∈ x43 ⟶ ∀ x46 . x46 ⊆ setminus x43 (Sing x45) ⟶ ∀ x47 . x47 ∈ x46 ⟶ ∀ x48 . x48 ∈ x46 ⟶ ∀ x49 . x49 ∈ x46 ⟶ ∀ x50 . x50 ∈ x46 ⟶ ∀ x51 . x51 ∈ x46 ⟶ ∀ x52 . x52 ∈ x46 ⟶ ∀ x53 . x53 ∈ x46 ⟶ ∀ x54 . x54 ∈ x46 ⟶ ∀ x55 . x55 ∈ x46 ⟶ x42 x44 x47 x48 x49 x50 x51 x52 x53 x54 x55 ⟶ 5bab1.. x43 x44) ⟶ ∀ x43 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x44 . ∀ x45 : ι → ι → ο . (∀ x46 . x46 ∈ x44 ⟶ ∀ x47 . x47 ∈ x44 ⟶ x45 x46 x47 ⟶ x45 x47 x46) ⟶ 4402e.. x44 x45 ⟶ cf2df.. x44 x45 ⟶ ∀ x46 . x46 ∈ x44 ⟶ ∀ x47 . x47 ⊆ setminus x44 (Sing x46) ⟶ ∀ x48 . x48 ∈ x47 ⟶ ∀ x49 . x49 ∈ x47 ⟶ ∀ x50 . x50 ∈ x47 ⟶ ∀ x51 . x51 ∈ x47 ⟶ ∀ x52 . x52 ∈ x47 ⟶ ∀ x53 . x53 ∈ x47 ⟶ ∀ x54 . x54 ∈ x47 ⟶ ∀ x55 . x55 ∈ x47 ⟶ ∀ x56 . x56 ∈ x47 ⟶ x43 x45 x48 x49 x50 x51 x52 x53 x54 x55 x56 ⟶ 5bab1.. x44 x45) ⟶ ∀ x44 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x45 . ∀ x46 : ι → ι → ο . (∀ x47 . x47 ∈ x45 ⟶ ∀ x48 . x48 ∈ x45 ⟶ x46 x47 x48 ⟶ x46 x48 x47) ⟶ 4402e.. x45 x46 ⟶ cf2df.. x45 x46 ⟶ ∀ x47 . x47 ∈ x45 ⟶ ∀ x48 . x48 ⊆ setminus x45 (Sing x47) ⟶ ∀ x49 . x49 ∈ x48 ⟶ ∀ x50 . x50 ∈ x48 ⟶ ∀ x51 . x51 ∈ x48 ⟶ ∀ x52 . x52 ∈ x48 ⟶ ∀ x53 . x53 ∈ x48 ⟶ ∀ x54 . x54 ∈ x48 ⟶ ∀ x55 . x55 ∈ x48 ⟶ ∀ x56 . x56 ∈ x48 ⟶ ∀ x57 . x57 ∈ x48 ⟶ x44 x46 x49 x50 x51 x52 x53 x54 x55 x56 x57 ⟶ 5bab1.. x45 x46) ⟶ ∀ x45 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x46 . ∀ x47 : ι → ι → ο . (∀ x48 . x48 ∈ x46 ⟶ ∀ x49 . x49 ∈ x46 ⟶ x47 x48 x49 ⟶ x47 x49 x48) ⟶ 4402e.. x46 x47 ⟶ cf2df.. x46 x47 ⟶ ∀ x48 . x48 ∈ x46 ⟶ ∀ x49 . x49 ⊆ setminus x46 (Sing x48) ⟶ ∀ x50 . x50 ∈ x49 ⟶ ∀ x51 . x51 ∈ x49 ⟶ ∀ x52 . x52 ∈ x49 ⟶ ∀ x53 . x53 ∈ x49 ⟶ ∀ x54 . x54 ∈ x49 ⟶ ∀ x55 . x55 ∈ x49 ⟶ ∀ x56 . x56 ∈ x49 ⟶ ∀ x57 . x57 ∈ x49 ⟶ ∀ x58 . x58 ∈ x49 ⟶ x45 x47 x50 x51 x52 x53 x54 x55 x56 x57 x58 ⟶ 5bab1.. x46 x47) ⟶ ∀ x46 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x47 . ∀ x48 : ι → ι → ο . (∀ x49 . x49 ∈ x47 ⟶ ∀ x50 . x50 ∈ x47 ⟶ x48 x49 x50 ⟶ x48 x50 x49) ⟶ 4402e.. x47 x48 ⟶ cf2df.. x47 x48 ⟶ ∀ x49 . x49 ∈ x47 ⟶ ∀ x50 . x50 ⊆ setminus x47 (Sing x49) ⟶ ∀ x51 . x51 ∈ x50 ⟶ ∀ x52 . x52 ∈ x50 ⟶ ∀ x53 . x53 ∈ x50 ⟶ ∀ x54 . x54 ∈ x50 ⟶ ∀ x55 . x55 ∈ x50 ⟶ ∀ x56 . x56 ∈ x50 ⟶ ∀ x57 . x57 ∈ x50 ⟶ ∀ x58 . x58 ∈ x50 ⟶ ∀ x59 . x59 ∈ x50 ⟶ x46 x48 x51 x52 x53 x54 x55 x56 x57 x58 x59 ⟶ 5bab1.. x47 x48) ⟶ ∀ x47 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x48 . ∀ x49 : ι → ι → ο . (∀ x50 . x50 ∈ x48 ⟶ ∀ x51 . x51 ∈ x48 ⟶ x49 x50 x51 ⟶ x49 x51 x50) ⟶ 4402e.. x48 x49 ⟶ cf2df.. x48 x49 ⟶ ∀ x50 . x50 ∈ x48 ⟶ ∀ x51 . x51 ⊆ setminus x48 (Sing x50) ⟶ ∀ x52 . x52 ∈ x51 ⟶ ∀ x53 . x53 ∈ x51 ⟶ ∀ x54 . x54 ∈ x51 ⟶ ∀ x55 . x55 ∈ x51 ⟶ ∀ x56 . x56 ∈ x51 ⟶ ∀ x57 . x57 ∈ x51 ⟶ ∀ x58 . x58 ∈ x51 ⟶ ∀ x59 . x59 ∈ x51 ⟶ ∀ x60 . x60 ∈ x51 ⟶ x47 x49 x52 x53 x54 x55 x56 x57 x58 x59 x60 ⟶ 5bab1.. x48 x49) ⟶ ∀ x48 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x49 . ∀ x50 : ι → ι → ο . (∀ x51 . x51 ∈ x49 ⟶ ∀ x52 . x52 ∈ x49 ⟶ x50 x51 x52 ⟶ x50 x52 x51) ⟶ 4402e.. x49 x50 ⟶ cf2df.. x49 x50 ⟶ ∀ x51 . x51 ∈ x49 ⟶ ∀ x52 . x52 ⊆ setminus x49 (Sing x51) ⟶ ∀ x53 . x53 ∈ x52 ⟶ ∀ x54 . x54 ∈ x52 ⟶ ∀ x55 . x55 ∈ x52 ⟶ ∀ x56 . x56 ∈ x52 ⟶ ∀ x57 . x57 ∈ x52 ⟶ ∀ x58 . x58 ∈ x52 ⟶ ∀ x59 . x59 ∈ x52 ⟶ ∀ x60 . x60 ∈ x52 ⟶ ∀ x61 . x61 ∈ x52 ⟶ x48 x50 x53 x54 x55 x56 x57 x58 x59 x60 x61 ⟶ 5bab1.. x49 x50) ⟶ ∀ x49 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x50 . ∀ x51 : ι → ι → ο . (∀ x52 . x52 ∈ x50 ⟶ ∀ x53 . x53 ∈ x50 ⟶ x51 x52 x53 ⟶ x51 x53 x52) ⟶ 4402e.. x50 x51 ⟶ cf2df.. x50 x51 ⟶ ∀ x52 . x52 ∈ x50 ⟶ ∀ x53 . x53 ⊆ setminus x50 (Sing x52) ⟶ ∀ x54 . x54 ∈ x53 ⟶ ∀ x55 . x55 ∈ x53 ⟶ ∀ x56 . x56 ∈ x53 ⟶ ∀ x57 . x57 ∈ x53 ⟶ ∀ x58 . x58 ∈ x53 ⟶ ∀ x59 . x59 ∈ x53 ⟶ ∀ x60 . x60 ∈ x53 ⟶ ∀ x61 . x61 ∈ x53 ⟶ ∀ x62 . x62 ∈ x53 ⟶ x49 x51 x54 x55 x56 x57 x58 x59 x60 x61 x62 ⟶ 5bab1.. x50 x51) ⟶ ∀ x50 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x51 . ∀ x52 : ι → ι → ο . (∀ x53 . x53 ∈ x51 ⟶ ∀ x54 . x54 ∈ x51 ⟶ x52 x53 x54 ⟶ x52 x54 x53) ⟶ 4402e.. x51 x52 ⟶ cf2df.. x51 x52 ⟶ ∀ x53 . x53 ∈ x51 ⟶ ∀ x54 . x54 ⊆ setminus x51 (Sing x53) ⟶ ∀ x55 . x55 ∈ x54 ⟶ ∀ x56 . x56 ∈ x54 ⟶ ∀ x57 . x57 ∈ x54 ⟶ ∀ x58 . x58 ∈ x54 ⟶ ∀ x59 . x59 ∈ x54 ⟶ ∀ x60 . x60 ∈ x54 ⟶ ∀ x61 . x61 ∈ x54 ⟶ ∀ x62 . x62 ∈ x54 ⟶ ∀ x63 . x63 ∈ x54 ⟶ x50 x52 x55 x56 x57 x58 x59 x60 x61 x62 x63 ⟶ 5bab1.. x51 x52) ⟶ ∀ x51 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x52 . ∀ x53 : ι → ι → ο . (∀ x54 . x54 ∈ x52 ⟶ ∀ x55 . x55 ∈ x52 ⟶ x53 x54 x55 ⟶ x53 x55 x54) ⟶ 4402e.. x52 x53 ⟶ cf2df.. x52 x53 ⟶ ∀ x54 . x54 ∈ x52 ⟶ ∀ x55 . x55 ⊆ setminus x52 (Sing x54) ⟶ ∀ x56 . x56 ∈ x55 ⟶ ∀ x57 . x57 ∈ x55 ⟶ ∀ x58 . x58 ∈ x55 ⟶ ∀ x59 . x59 ∈ x55 ⟶ ∀ x60 . x60 ∈ x55 ⟶ ∀ x61 . x61 ∈ x55 ⟶ ∀ x62 . x62 ∈ x55 ⟶ ∀ x63 . x63 ∈ x55 ⟶ ∀ x64 . x64 ∈ x55 ⟶ x51 x53 x56 x57 x58 x59 x60 x61 x62 x63 x64 ⟶ 5bab1.. x52 x53) ⟶ ∀ x52 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x53 . ∀ x54 : ι → ι → ο . (∀ x55 . x55 ∈ x53 ⟶ ∀ x56 . x56 ∈ x53 ⟶ x54 x55 x56 ⟶ x54 x56 x55) ⟶ 4402e.. x53 x54 ⟶ cf2df.. x53 x54 ⟶ ∀ x55 . x55 ∈ x53 ⟶ ∀ x56 . x56 ⊆ setminus x53 (Sing x55) ⟶ ∀ x57 . x57 ∈ x56 ⟶ ∀ x58 . x58 ∈ x56 ⟶ ∀ x59 . x59 ∈ x56 ⟶ ∀ x60 . x60 ∈ x56 ⟶ ∀ x61 . x61 ∈ x56 ⟶ ∀ x62 . x62 ∈ x56 ⟶ ∀ x63 . x63 ∈ x56 ⟶ ∀ x64 . x64 ∈ x56 ⟶ ∀ x65 . x65 ∈ x56 ⟶ x52 x54 x57 x58 x59 x60 x61 x62 x63 x64 x65 ⟶ 5bab1.. x53 x54) ⟶ ∀ x53 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x54 . ∀ x55 : ι → ι → ο . (∀ x56 . x56 ∈ x54 ⟶ ∀ x57 . x57 ∈ x54 ⟶ x55 x56 x57 ⟶ x55 x57 x56) ⟶ 4402e.. x54 x55 ⟶ cf2df.. x54 x55 ⟶ ∀ x56 . x56 ∈ x54 ⟶ ∀ x57 . x57 ⊆ setminus x54 (Sing x56) ⟶ ∀ x58 . x58 ∈ x57 ⟶ ∀ x59 . x59 ∈ x57 ⟶ ∀ x60 . x60 ∈ x57 ⟶ ∀ x61 . x61 ∈ x57 ⟶ ∀ x62 . x62 ∈ x57 ⟶ ∀ x63 . x63 ∈ x57 ⟶ ∀ x64 . x64 ∈ x57 ⟶ ∀ x65 . x65 ∈ x57 ⟶ ∀ x66 . x66 ∈ x57 ⟶ x53 x55 x58 x59 x60 x61 x62 x63 x64 x65 x66 ⟶ 5bab1.. x54 x55) ⟶ ∀ x54 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x55 . ∀ x56 : ι → ι → ο . (∀ x57 . x57 ∈ x55 ⟶ ∀ x58 . x58 ∈ x55 ⟶ x56 x57 x58 ⟶ x56 x58 x57) ⟶ 4402e.. x55 x56 ⟶ cf2df.. x55 x56 ⟶ ∀ x57 . x57 ∈ x55 ⟶ ∀ x58 . x58 ⊆ setminus x55 (Sing x57) ⟶ ∀ x59 . x59 ∈ x58 ⟶ ∀ x60 . x60 ∈ x58 ⟶ ∀ x61 . x61 ∈ x58 ⟶ ∀ x62 . x62 ∈ x58 ⟶ ∀ x63 . x63 ∈ x58 ⟶ ∀ x64 . x64 ∈ x58 ⟶ ∀ x65 . x65 ∈ x58 ⟶ ∀ x66 . x66 ∈ x58 ⟶ ∀ x67 . x67 ∈ x58 ⟶ x54 x56 x59 x60 x61 x62 x63 x64 x65 x66 x67 ⟶ 5bab1.. x55 x56) ⟶ ∀ x55 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x56 . ∀ x57 : ι → ι → ο . (∀ x58 . x58 ∈ x56 ⟶ ∀ x59 . x59 ∈ x56 ⟶ x57 x58 x59 ⟶ x57 x59 x58) ⟶ 4402e.. x56 x57 ⟶ cf2df.. x56 x57 ⟶ ∀ x58 . x58 ∈ x56 ⟶ ∀ x59 . x59 ⊆ setminus x56 (Sing x58) ⟶ ∀ x60 . x60 ∈ x59 ⟶ ∀ x61 . x61 ∈ x59 ⟶ ∀ x62 . x62 ∈ x59 ⟶ ∀ x63 . x63 ∈ x59 ⟶ ∀ x64 . x64 ∈ x59 ⟶ ∀ x65 . x65 ∈ x59 ⟶ ∀ x66 . x66 ∈ x59 ⟶ ∀ x67 . x67 ∈ x59 ⟶ ∀ x68 . x68 ∈ x59 ⟶ x55 x57 x60 x61 x62 x63 x64 x65 x66 x67 x68 ⟶ 5bab1.. x56 x57) ⟶ ∀ x56 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x57 . ∀ x58 : ι → ι → ο . (∀ x59 . x59 ∈ x57 ⟶ ∀ x60 . x60 ∈ x57 ⟶ x58 x59 x60 ⟶ x58 x60 x59) ⟶ 4402e.. x57 x58 ⟶ cf2df.. x57 x58 ⟶ ∀ x59 . x59 ∈ x57 ⟶ ∀ x60 . x60 ⊆ setminus x57 (Sing x59) ⟶ ∀ x61 . x61 ∈ x60 ⟶ ∀ x62 . x62 ∈ x60 ⟶ ∀ x63 . x63 ∈ x60 ⟶ ∀ x64 . x64 ∈ x60 ⟶ ∀ x65 . x65 ∈ x60 ⟶ ∀ x66 . x66 ∈ x60 ⟶ ∀ x67 . x67 ∈ x60 ⟶ ∀ x68 . x68 ∈ x60 ⟶ ∀ x69 . x69 ∈ x60 ⟶ x56 x58 x61 x62 x63 x64 x65 x66 x67 x68 x69 ⟶ 5bab1.. x57 x58) ⟶ ∀ x57 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x58 . ∀ x59 : ι → ι → ο . (∀ x60 . x60 ∈ x58 ⟶ ∀ x61 . x61 ∈ x58 ⟶ x59 x60 x61 ⟶ x59 x61 x60) ⟶ 4402e.. x58 x59 ⟶ cf2df.. x58 x59 ⟶ ∀ x60 . x60 ∈ x58 ⟶ ∀ x61 . x61 ⊆ setminus x58 (Sing x60) ⟶ ∀ x62 . x62 ∈ x61 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ ∀ x65 . x65 ∈ x61 ⟶ ∀ x66 . x66 ∈ x61 ⟶ ∀ x67 . x67 ∈ x61 ⟶ ∀ x68 . x68 ∈ x61 ⟶ ∀ x69 . x69 ∈ x61 ⟶ ∀ x70 . x70 ∈ x61 ⟶ x57 x59 x62 x63 x64 x65 x66 x67 x68 x69 x70 ⟶ 5bab1.. x58 x59) ⟶ ∀ x58 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x59 . ∀ x60 : ι → ι → ο . (∀ x61 . x61 ∈ x59 ⟶ ∀ x62 . x62 ∈ x59 ⟶ x60 x61 x62 ⟶ x60 x62 x61) ⟶ 4402e.. x59 x60 ⟶ cf2df.. x59 x60 ⟶ ∀ x61 . x61 ∈ x59 ⟶ ∀ x62 . x62 ⊆ setminus x59 (Sing x61) ⟶ ∀ x63 . x63 ∈ x62 ⟶ ∀ x64 . x64 ∈ x62 ⟶ ∀ x65 . x65 ∈ x62 ⟶ ∀ x66 . x66 ∈ x62 ⟶ ∀ x67 . x67 ∈ x62 ⟶ ∀ x68 . x68 ∈ x62 ⟶ ∀ x69 . x69 ∈ x62 ⟶ ∀ x70 . x70 ∈ x62 ⟶ ∀ x71 . x71 ∈ x62 ⟶ x58 x60 x63 x64 x65 x66 x67 x68 x69 x70 x71 ⟶ 5bab1.. x59 x60) ⟶ ∀ x59 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x60 . ∀ x61 : ι → ι → ο . (∀ x62 . x62 ∈ x60 ⟶ ∀ x63 . x63 ∈ x60 ⟶ x61 x62 x63 ⟶ x61 x63 x62) ⟶ 4402e.. x60 x61 ⟶ cf2df.. x60 x61 ⟶ ∀ x62 . x62 ∈ x60 ⟶ ∀ x63 . x63 ⊆ setminus x60 (Sing x62) ⟶ ∀ x64 . x64 ∈ x63 ⟶ ∀ x65 . x65 ∈ x63 ⟶ ∀ x66 . x66 ∈ x63 ⟶ ∀ x67 . x67 ∈ x63 ⟶ ∀ x68 . x68 ∈ x63 ⟶ ∀ x69 . x69 ∈ x63 ⟶ ∀ x70 . x70 ∈ x63 ⟶ ∀ x71 . x71 ∈ x63 ⟶ ∀ x72 . x72 ∈ x63 ⟶ x59 x61 x64 x65 x66 x67 x68 x69 x70 x71 x72 ⟶ 5bab1.. x60 x61) ⟶ ∀ x60 : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ο . (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ x60 x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 654b9.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 7e5de.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ a3794.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 093ca.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 34ae8.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 96162.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 3c407.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ d92ce.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 105be.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ a2064.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ f5da9.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b9a4e.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 6e81c.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 4e91d.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 8c9ed.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 37e04.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 13b7c.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 2bf4d.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 53286.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 7db3a.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 22587.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 4d3d7.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ de118.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b0749.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 54c7d.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ cf078.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b43ab.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 96c31.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 627df.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 74622.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 3f98b.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ a0d70.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ dbf71.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ f842a.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 23b40.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ d5d69.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 2e1d5.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 94f0c.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 923e2.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 1a9fd.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b39ef.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 0788d.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ e2ec9.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 65996.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 45286.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 8bd80.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 729bd.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 76a6c.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 8d9b1.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 1668d.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ c4d5c.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ e37fb.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ e8ba7.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 7f17b.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ d2e51.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 9eede.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 150dd.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 2c550.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 286f8.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b8d2a.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 05795.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 59a16.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ cec27.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ ba960.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ c2e8a.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ adf05.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 07c0f.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b7a83.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 74a95.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ fc090.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 72d65.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ b7e1a.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ e5024.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 91113.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ f0823.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ a9907.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 4b4dd.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ a47b6.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ aa358.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ ee649.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 57f60.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ a7e88.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ 59632.. x62 x65 x66 x67 x68 x69 x70 x71 x72 x73 ⟶ 5bab1.. x61 x62) ⟶ (∀ x61 . ∀ x62 : ι → ι → ο . (∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ∈ x61 ⟶ x62 x63 x64 ⟶ x62 x64 x63) ⟶ 4402e.. x61 x62 ⟶ cf2df.. x61 x62 ⟶ ∀ x63 . x63 ∈ x61 ⟶ ∀ x64 . x64 ⊆ setminus x61 (Sing x63) ⟶ ∀ x65 . x65 ∈ x64 ⟶ ∀ x66 . x66 ∈ x64 ⟶ ∀ x67 . x67 ∈ x64 ⟶ ∀ x68 . x68 ∈ x64 ⟶ ∀ x69 . x69 ∈ x64 ⟶ ∀ x70 . x70 ∈ x64 ⟶ ∀ x71 . x71 ∈ x64 ⟶ ∀ x72 . x72 ∈ x64 ⟶ ∀ x73 . x73 ∈ x64 ⟶ |
|