| λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x6 x4 x7)) (x1 x6 x5 x8)) (x0 x9)) (x1 x4 x9 x10)) (x1 x5 x9 x11)) (x3 x6 x4 x9 x10 x7 = x3 x6 x5 x9 x11 x8)) (∀ x13 . x0 x13 ⟶ ∀ x14 . x1 x4 x13 x14 ⟶ ∀ x15 . x1 x5 x13 x15 ⟶ x3 x6 x4 x13 x14 x7 = x3 x6 x5 x13 x15 x8 ⟶ and (and (and (x1 x9 x13 (x12 x13 x14 x15)) (x3 x4 x9 x13 (x12 x13 x14 x15) x10 = x14)) (x3 x5 x9 x13 (x12 x13 x14 x15) x11 = x15)) (∀ x16 . x1 x9 x13 x16 ⟶ x3 x4 x9 x13 x16 x10 = x14 ⟶ x3 x5 x9 x13 x16 x11 = x15 ⟶ x16 = x12 x13 x14 x15)) |
|