Proofgold Proof

Apply H0 with x1, λ x3 . (λ x4 x5 x6 x7 x8 . λ x9 : ι → ι → ι → ι . and (and (UnaryPredHom x4 x6 x7) (UnaryPredHom x5 x6 x8)) (∀ x10 . x0 x10 ⟶ ∀ x11 x12 . UnaryPredHom x4 x10 x11 ⟶ UnaryPredHom x5 x10 x12 ⟶ and (and (and (UnaryPredHom x6 x10 (x9 x10 x11 x12)) (struct_comp x4 x6 x10 (x9 x10 x11 x12) x7 = x11)) (struct_comp x5 x6 x10 (x9 x10 x11 x12) x8 = x12)) (∀ x13 . UnaryPredHom x6 x10 x13 ⟶ struct_comp x4 x6 x10 x13 x7 = x11 ⟶ struct_comp x5 x6 x10 x13 x8 = x12 ⟶ x13 = x9 x10 x11 x12))) x3 x2 (20e9b.. x3 x2) (lam (ap x3 0) (λ x4 . Inj0 x4)) (lam (ap x2 0) (λ x4 . Inj1 x4)) (λ x4 x5 x6 . lam (setsum (ap x3 0) (ap x2 0)) (λ x7 . combine_funcs (ap x3 0) (ap x2 0) (λ x8 . ap x5 x8) (λ x8 . ap x6 x8) x7)), MetaCat_coproduct_p x0 UnaryPredHom struct_id struct_comp x1 x2 (20e9b.. x1 x2) (lam (ap x1 0) (λ x3 . Inj0 x3)) (lam (ap x2 0) (λ x3 . Inj1 x3)) (λ x3 x4 x5 . lam (setsum (ap x1 0) (ap x2 0)) (λ x6 . combine_funcs (ap x1 0) (ap x2 0) (λ x7 . ap x4 x7) (λ x7 . ap x5 x7) x6)) leaving 3 subgoals.