Apply unknownprop_6482952e7e0a4bf00d28fb92ecd380f707bb40e0d65cb44f18a4b021cf4cfdbf with ∃ x0 . ∃ x1 : ι → ι . MetaCat_initial_p 9f253.. UnaryFuncHom struct_id struct_comp x0 x1.

Let x0 of type ι be given.

Assume H0: (λ x1 . ∃ x2 : ι → ι . MetaCat_initial_p (λ x3 . True) HomSet (λ x3 . lam x3 (λ x4 . x4)) (λ x3 x4 x5 x6 x7 . lam x3 (λ x8 . ap x6 (ap x7 x8))) x1 x2) x0.

Apply H0 with ∃ x1 . ∃ x2 : ι → ι . MetaCat_initial_p 9f253.. UnaryFuncHom struct_id struct_comp x1 x2.

Let x1 of type ι → ι be given.

Assume H1: MetaCat_initial_p (λ x2 . True) HomSet (λ x2 . lam x2 (λ x3 . x3)) (λ x2 x3 x4 x5 x6 . lam x2 (λ x7 . ap x5 (ap x6 x7))) x0 x1.

Let x2 of type ο be given.

Assume H2: ∀ x3 . (∃ x4 : ι → ι . MetaCat_initial_p 9f253.. UnaryFuncHom struct_id struct_comp x3 x4) ⟶ x2.

Apply H2 with (λ x3 . pack_u (setsum x3 x3) (combine_funcs x3 x3 Inj1 Inj1)) x0.

Apply unknownprop_9e4a4e86d499216c8785bdcb6ea98c9ec4aee7ee82bde465e88bf0a451f2bef0 with λ x3 . True, HomSet, λ x3 . lam x3 (λ x4 . x4), λ x3 x4 x5 x6 x7 . lam x3 (λ x8 . ap x6 (ap x7 x8)), 9f253.., UnaryFuncHom, struct_id, struct_comp, λ x3 . pack_u (setsum x3 x3) (combine_funcs x3 x3 Inj1 Inj1), λ x3 x4 x5 . lam (setsum x3 x3) (λ x6 . combine_funcs x3 x3 (λ x7 . Inj0 (ap x5 x7)) (λ x7 . Inj1 (ap x5 x7)) x6), λ x3 . ap x3 0, λ x3 x4 x5 . x5, λ x3 . lam x3 (λ x4 . Inj0 x4), λ x3 . unpack_u_i x3 (λ x4 . λ x5 : ι → ι . lam (setsum x4 x4) (λ x6 . combine_funcs x4 x4 (λ x7 . x7) x5 x6)), x0, x1 leaving 2 subgoals.

The subproof is completed by applying unknownprop_cc47c963ab9cc0e5e798780a66a4301b5c1e3c6b4bcc2abf1af8a16f9b487402.

The subproof is completed by applying H1.

■

Proofgold Proof