Let x0 of type ι → ο be given.
Let x1 of type ι → ι → ι → ο be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι → ι → ι → ι → ι be given.
Let x4 of type ι → ι → ι be given.
Let x5 of type ι → ι → ι be given.
Let x6 of type ι → ι → ι be given.
Let x7 of type ι → ι → ι → ι → ι → ι be given.
Assume H0:
∀ 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.
Let x8 of type ι be given.
Let x9 of type ι be given.
Assume H1: x0 x8.
Assume H2: x0 x9.
Apply H0 with
x8,
x9,
MetaCat_product_p x0 x1 x2 x3 x8 x9 (x4 x8 x9) (x5 x8 x9) (x6 x8 x9) (x7 x8 x9) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Assume H3: x0 (x4 x8 x9).
Assume H4: x1 (x4 x8 x9) x8 (x5 x8 x9).
Assume H5: x1 (x4 x8 x9) x9 (x6 x8 x9).
Assume H6:
∀ x10 . ... ⟶ ∀ x11 x12 . ... ⟶ ... ⟶ and (and (and (x1 x10 (x4 x8 x9) (x7 x8 x9 x10 x11 x12)) (x3 x10 (x4 x8 x9) x8 (x5 x8 x9) (x7 x8 x9 x10 x11 x12) = x11)) (x3 x10 (x4 x8 x9) x9 (x6 x8 x9) (x7 x8 x9 x10 x11 x12) = x12)) (∀ x13 . ... ⟶ x3 x10 (x4 x8 ...) ... ... ... = ... ⟶ x3 x10 (x4 x8 x9) x9 (x6 x8 x9) x13 = x12 ⟶ x13 = x7 x8 x9 x10 x11 x12).