Let x0 of type ο be given.

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

Apply H0 with pack_p 1 (λ x1 . True).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι . (∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_p UnaryPredHom struct_id struct_comp (pack_p 1 (λ x7 . True)) 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_p UnaryPredHom struct_id struct_comp (pack_p 1 (λ x7 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) x3 x4 x5 x6) ⟶ x2.

Apply H2 with pack_p omega (λ x3 . True).

Let x3 of type ο be given.

Assume H3: ∀ x4 . (∃ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p struct_p UnaryPredHom struct_id struct_comp (pack_p 1 (λ x7 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_p omega (λ x7 . True)) 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_p UnaryPredHom struct_id struct_comp (pack_p 1 (λ x7 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_p omega (λ x7 . True)) (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_p UnaryPredHom struct_id struct_comp (pack_p 1 (λ x7 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_p omega (λ x7 . True)) (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).

Claim L6: struct_p (pack_p 1 (λ x6 . True))

The subproof is completed by applying pack_struct_p_I with 1, λ x6 . True.

Claim L7: struct_p (pack_p omega (λ x6 . True))

The subproof is completed by applying pack_struct_p_I with omega, λ x6 . True.

Apply unknownprop_87e4b92e864cd20cb66a704125e89f2601312b49a571aa5aeba3f0ceb096da6e with struct_p leaving 3 subgoals.

Let x6 of type ι be given.

Assume H8: struct_p x6.

The subproof is completed by applying H8.

The subproof is completed by applying L6.

The subproof is completed by applying L7.

■

Proofgold Proof