Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι → ι . (∃ x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_p UnaryPredHom struct_id struct_comp x1 x2 x3 x4) ⟶ x0.

Apply H0 with 20e9b...

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι . (∃ x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_p UnaryPredHom struct_id struct_comp 20e9b.. x2 x3 x4) ⟶ x1.

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

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι → ι . (∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_p UnaryPredHom struct_id struct_comp 20e9b.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) x3 x4) ⟶ x2.

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

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p struct_p UnaryPredHom struct_id struct_comp 20e9b.. (λ x5 x6 . lam (ap x5 0) (λ x7 . Inj0 x7)) (λ x5 x6 . lam (ap x6 0) (λ x7 . Inj1 x7)) x4 ⟶ x3.

Apply H3 with λ x4 x5 x6 x7 x8 . lam (setsum (ap x4 0) (ap x5 0)) (λ x9 . combine_funcs (ap x4 0) (ap x5 0) (λ x10 . ap x7 x10) (λ x10 . ap x8 x10) x9).

Apply unknownprop_eb8fa85f1ab6d587c913965e3b03d2a9bd8d29f88f55fc57c7ee9d90282aeead with struct_p leaving 2 subgoals.

Let x4 of type ι be given.

Assume H4: struct_p x4.

The subproof is completed by applying H4.

The subproof is completed by applying unknownprop_1173f252c04f1e26dd932c58949a3d54b001764c56ceceb60de241154a660c4d.

■

Proofgold Proof