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