Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . ∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_u UnaryFuncHom struct_id struct_comp x1 x2 x3 x4 x5 x6) ⟶ x0.

Apply H0 with pack_u 1 (λ x1 . 0).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . (∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x7 . 0)) x2 x3 x4 x5 x6) ⟶ x1.

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

Let x2 of type ο be given.

Assume H2: ∀ x3 . (∃ x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x7 . 0)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) x3 x4 x5 x6) ⟶ x2.

Apply H2 with pack_u omega (λ x3 . x3).

Let x3 of type ο be given.

Assume H3: ∀ x4 . (∃ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x7 . 0)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_u omega (λ x7 . x7)) x4 x5 x6) ⟶ x3.

Apply H3 with lam 1 (λ x4 . 0).

Let x4 of type ο be given.

Assume H4: ∀ x5 . (∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x7 . 0)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_u omega (λ x7 . x7)) (lam 1 (λ x7 . 0)) x5 x6) ⟶ x4.

Apply H4 with lam omega (λ x5 . ordsucc x5).

Let x5 of type ο be given.

Assume H5: ∀ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x7 . 0)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_u omega (λ x7 . x7)) (lam 1 (λ x7 . 0)) (lam omega (λ x7 . ordsucc x7)) x6 ⟶ x5.

Apply H5 with λ x6 x7 x8 . lam omega (λ x9 . nat_primrec (ap x7 0) (λ x10 x11 . ap x8 x11) x9).

Apply and5I with MetaCat_terminal_p struct_u UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x6 . 0)) (λ x6 . lam (ap x6 0) (λ x7 . 0)), struct_u (pack_u omega (λ x6 . x6)), UnaryFuncHom (pack_u 1 (λ x6 . 0)) (pack_u omega (λ x6 . x6)) (lam 1 (λ x6 . 0)), UnaryFuncHom (pack_u omega (λ x6 . x6)) (pack_u omega (λ x6 . x6)) (lam omega (λ x6 . ordsucc x6)), ∀ x6 x7 x8 . ... ⟶ ... ⟶ ... ⟶ and (and (and (UnaryFuncHom (pack_u omega (λ x9 . x9)) x6 ((λ x9 x10 x11 . lam omega (λ x12 . nat_primrec (ap ... 0) ... ...)) ... ... ...)) ...) ...) ... leaving 5 subgoals.

...

■

Proofgold Proof