Claim L0: ...

...

Claim L1: ...

...

Claim L2: ...

...

Claim L3: ...

...

Claim L4: ...

...

Apply L1 with ∃ x0 x1 x2 : ι → ι → ι . ∃ x3 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x0 x1 x2 x3.

Let x0 of type ι → ι → ι be given.

Assume H5: (λ x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . ∀ x5 : ι → ι . (∀ x6 . x6 ∈ x4 ⟶ x5 x6 ∈ x4) ⟶ x1 (pack_u x2 x3) (pack_u x4 x5) = pack_u (setprod x2 x4) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (x3 (ap x6 0)) (x5 (ap x6 1))))) x0.

Apply L2 with ∃ x1 x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x1 x2 x3 x4.

Let x1 of type ι → ι → ι be given.

Assume H6: (λ x2 : ι → ι → ι . ∀ x3 . ∀ x4 : ι → ι . ∀ x5 . ∀ x6 : ι → ι . x2 (pack_u x3 x4) (pack_u x5 x6) = lam (setprod x3 x5) (λ x7 . ap x7 0)) x1.

Apply L3 with ∃ x2 x3 x4 : ι → ι → ι . ∃ x5 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x2 x3 x4 x5.

Let x2 of type ι → ι → ι be given.

Assume H7: (λ x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι . ∀ x6 . ∀ x7 : ι → ι . x3 (pack_u x4 x5) (pack_u x6 x7) = lam (setprod x4 x6) (λ x8 . ap x8 1)) x2.

Apply L4 with ∃ x3 x4 x5 : ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x3 x4 x5 x6.

Let x3 of type ι → ι → ι → ι → ι → ι be given.

Assume H8: (λ x4 : ι → ι → ι → ι → ι → ι . ∀ x5 x6 x7 . ∀ x8 : ι → ι . ∀ x9 x10 . x4 x5 x6 (pack_u x7 x8) x9 x10 = lam x7 (λ x11 . lam 2 (λ x12 . If_i (x12 = 0) (ap x9 x11) (ap x10 x11)))) x3.

Claim L9: ...

...

Let x4 of type ο be given.

Assume H10: ∀ x5 : ι → ι → ι . (∃ x6 x7 : ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x5 x6 x7 x8) ⟶ x4.

Apply H10 with x0.

Let x5 of type ο be given.

Assume H11: ∀ x6 : ι → ι → ι . (∃ x7 : ι → ι → ι . ∃ x8 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x0 x6 x7 x8) ⟶ x5.

Apply H11 with x1.

Let x6 of type ο be given.

Assume H12: ∀ x7 : ι → ι → ι . (∃ x8 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x0 x1 x7 x8) ⟶ x6.

Apply H12 with x2.

Let x7 of type ο be given.

Assume H13: ∀ x8 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p 9f253.. UnaryFuncHom struct_id struct_comp x0 x1 x2 x8 ⟶ x7.

Apply H13 with x3.

Apply unknownprop_b44bf17b712ca8b63c07a0ba06634caef680b43d449c8c8e8f92a801772b18d9 with 9f253.., UnaryFuncHom, struct_id, struct_comp, x0, x1, x2, x3.

Let x8 of type ι be given.

Let x9 of type ι be given.

Assume H14: 9f253.. x8.

Assume H15: 9f253.. x9.

Apply H14 with ∀ x10 : ο . (... ⟶ ... ⟶ ... ⟶ (∀ x11 . ... ⟶ ∀ x12 x13 . ... ⟶ ... ⟶ and (and (and (UnaryFuncHom x11 (x0 x8 x9) (x3 x8 x9 x11 x12 x13)) (struct_comp x11 (x0 x8 ...) ... ... ... = ...)) ...) ...) ⟶ x10) ⟶ x10.

...

■

Proofgold Proof