Let x0 of type ι → ο be given.

Let x1 of type ι → ι → ι → ο be given.

Let x2 of type ι → ι be given.

Let x3 of type ι → ι → ι → ι → ι → ι be given.

Assume H0: MetaCat x0 x1 x2 x3.

Let x4 of type ο be given.

Assume H1: MetaFunctor_prop1 x0 x1 x2 x3 ⟶ MetaFunctor_prop2 x0 x1 x2 x3 ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x5 x6 x7 (x2 x5) = x7) ⟶ (∀ x5 x6 x7 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 x6 x7 ⟶ x3 x5 x6 x6 (x2 x6) x7 = x7) ⟶ (∀ x5 x6 x7 x8 x9 x10 x11 . x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x1 x5 x6 x9 ⟶ x1 x6 x7 x10 ⟶ x1 x7 x8 x11 ⟶ x3 x5 x6 x8 (x3 x6 x7 x8 x11 x10) x9 = x3 x5 x7 x8 x11 (x3 x5 x6 x7 x10 x9)) ⟶ x4.

Apply H0 with x4.

Assume H2: and (and (MetaFunctor_prop1 x0 x1 x2 x3) (MetaFunctor_prop2 x0 x1 x2 x3)) (and (MetaCat_IdR_p x0 x1 x2 x3) (MetaCat_IdL_p x0 x1 x2 x3)).

Assume H3: MetaCat_Comp_assoc_p x0 x1 x2 x3.

Apply H2 with x4.

Assume H4: and (MetaFunctor_prop1 x0 x1 x2 x3) (MetaFunctor_prop2 x0 x1 x2 x3).

Assume H5: and (MetaCat_IdR_p x0 x1 x2 x3) (MetaCat_IdL_p x0 x1 x2 x3).

Apply H4 with x4.

Assume H6: MetaFunctor_prop1 x0 x1 x2 x3.

Assume H7: MetaFunctor_prop2 x0 x1 x2 x3.

Apply H5 with x4.

Assume H8: MetaCat_IdR_p x0 x1 x2 x3.

Assume H9: MetaCat_IdL_p x0 x1 x2 x3.

Apply H1 leaving 5 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

The subproof is completed by applying H9.

The subproof is completed by applying H3.

■

Proofgold Proof