Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι . (∃ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) 9f253.. UnaryFuncHom struct_id struct_comp x1 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x0.

Apply H0 with λ x1 . pack_u (setsum x1 x1) (combine_funcs x1 x1 Inj1 Inj1).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι → ι . (∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) 9f253.. UnaryFuncHom struct_id struct_comp (λ x5 . pack_u (setsum x5 x5) (combine_funcs x5 x5 Inj1 Inj1)) x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 x4 . lam (setsum x2 x2) (λ x5 . combine_funcs x2 x2 (λ x6 . Inj0 (ap x4 x6)) (λ x6 . Inj1 (ap x4 x6)) x5).

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι . (∃ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) 9f253.. UnaryFuncHom struct_id struct_comp (λ x5 . pack_u (setsum x5 x5) (combine_funcs x5 x5 Inj1 Inj1)) (λ x5 x6 x7 . lam (setsum x5 x5) (λ x8 . combine_funcs x5 x5 (λ x9 . Inj0 (ap x7 x9)) (λ x9 . Inj1 (ap x7 x9)) x8)) (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x2.

Apply H2 with λ x3 . lam x3 (λ x4 . Inj0 x4).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) 9f253.. UnaryFuncHom struct_id struct_comp (λ x5 . pack_u (setsum x5 x5) (combine_funcs x5 x5 Inj1 Inj1)) (λ x5 x6 x7 . lam (setsum x5 x5) (λ x8 . combine_funcs x5 x5 (λ x9 . Inj0 (ap x7 x9)) (λ x9 . Inj1 (ap x7 x9)) x8)) (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) (λ x5 . lam x5 (λ x6 . Inj0 x6)) x4 ⟶ x3.

Apply H3 with λ x4 . unpack_u_i x4 (λ x5 . λ x6 : ι → ι . lam (setsum x5 x5) (λ x7 . combine_funcs x5 x5 (λ x8 . x8) x6 x7)).

The subproof is completed by applying unknownprop_cc47c963ab9cc0e5e798780a66a4301b5c1e3c6b4bcc2abf1af8a16f9b487402.

■

Proofgold Proof