Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p SelfInjection UnaryFuncHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.

Apply H0 with 5a1fb...

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p SelfInjection UnaryFuncHom struct_id struct_comp 5a1fb.. x2 x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 . lam (setprod (ap x2 0) (ap x3 0)) (λ x4 . ap x4 0).

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p SelfInjection UnaryFuncHom struct_id struct_comp 5a1fb.. (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 0)) x3 x4) ⟶ x2.

Apply H2 with λ x3 x4 . lam (setprod (ap x3 0) (ap x4 0)) (λ x5 . ap x5 1).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p SelfInjection UnaryFuncHom struct_id struct_comp 5a1fb.. (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 0)) (λ x5 x6 . lam (setprod (ap x5 0) (ap x6 0)) (λ x7 . ap x7 1)) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 . lam (ap x6 0) (λ x9 . lam 2 (λ x10 . If_i (x10 = 0) (ap x7 x9) (ap x8 x9))).

Claim L4: ...

...

Claim L5: ∀ x4 x5 . SelfInjection x4 ⟶ SelfInjection x5 ⟶ SelfInjection (5a1fb.. x4 x5)

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H5: SelfInjection x4.

Assume H6: SelfInjection x5.

Apply unknownprop_2f1d491922dcc2c2c85957b7d88dc1d40484f0719168a164b34095ed29478f03 with x4, λ x6 . SelfInjection (5a1fb.. x6 x5) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x6 of type ι be given.

Let x7 of type ι → ι be given.

Assume H7: ∀ x8 . x8 ∈ x6 ⟶ x7 x8 ∈ x6.

Assume H8: ∀ x8 . x8 ∈ x6 ⟶ ∀ x9 . x9 ∈ x6 ⟶ x7 x8 = x7 x9 ⟶ x8 = x9.

Apply unknownprop_2f1d491922dcc2c2c85957b7d88dc1d40484f0719168a164b34095ed29478f03 with x5, λ x8 . SelfInjection (5a1fb.. (pack_u x6 x7) x8) leaving 2 subgoals.

The subproof is completed by applying H6.

Let x8 of type ι be given.

Let x9 of type ι → ι be given.

Assume H9: ∀ x10 . x10 ∈ x8 ⟶ x9 x10 ∈ x8.

Assume H10: ∀ x10 . x10 ∈ x8 ⟶ ∀ x11 . x11 ∈ x8 ⟶ x9 x10 = x9 x11 ⟶ x10 = x11.

Apply unknownprop_d4e4b2b932101a362c6dcbb7a861a9344a66a83ebdf6fb8c344e912c8c3c1d9a with x6, x7, x8, x9, λ x10 x11 . SelfInjection x11.

Apply unknownprop_afe4ec9c099d22c2baeaca2850cc89467409764fbc77a18c8ff75d652dbea36a with setprod x6 x8, λ x10 . lam 2 (λ x11 . If_i (x11 = 0) (x7 (ap x10 0)) (x9 (ap x10 1))) leaving 2 subgoals.

Let x10 of type ι be given.

Assume H11: x10 ∈ setprod x6 x8.

Apply tuple_2_Sigma with x6, λ x11 . x8, x7 (ap x10 0), x9 (ap x10 1) leaving 2 subgoals.

...

Apply unknownprop_885912b9bf5d57996dd171d0ae8acb2a108c6e54f48c2b0ffc8b58f100f1bbea with SelfInjection leaving 2 subgoals.

The subproof is completed by applying L4.

The subproof is completed by applying L5.

■

Proofgold Proof