Let x0 of type ο be given.

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

Apply H0 with pack_r 1 (λ x1 x2 . True).

Let x1 of type ο be given.

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

Apply H2 with pack_r omega (λ x3 x4 . x3 = x4).

Let x3 of type ο be given.

Assume H3: ∀ x4 . (∃ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p PER BinRelnHom struct_id struct_comp (pack_r 1 (λ x7 x8 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_r omega (λ x7 x8 . x7 = x8)) x4 x5 x6) ⟶ x3.

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

Let x4 of type ο be given.

Assume H4: ∀ x5 . (∃ x6 : ι → ι → ι → ι . MetaCat_nno_p PER BinRelnHom struct_id struct_comp (pack_r 1 (λ x7 x8 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_r omega (λ x7 x8 . x7 = x8)) (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 PER BinRelnHom struct_id struct_comp (pack_r 1 (λ x7 x8 . True)) (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_r omega (λ x7 x8 . x7 = x8)) (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: ...

...

Claim L7: ...

...

Claim L8: PER (pack_r omega (λ x6 x7 . x6 = x7))

Apply unknownprop_b2515235786361aea7c15ac6711d5751cd13b11988163a3b347abdb56aff828a with omega, λ x6 x7 . x6 = x7 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H8: x6 ∈ omega.

Let x7 of type ι be given.

Assume H9: x7 ∈ omega.

Assume H10: (λ x8 x9 . x8 = x9) x6 x7.

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

The subproof is completed by applying H10 with λ x9 x10 . x8 x10 x9.

Let x6 of type ι be given.

Assume H8: x6 ∈ omega.

Let x7 of type ι be given.

Assume H9: x7 ∈ omega.

Let x8 of type ι be given.

Assume H10: x8 ∈ omega.

Assume H11: (λ x9 x10 . x9 = x10) x6 x7.

Assume H12: (λ x9 x10 . x9 = x10) x7 ....

...

Apply unknownprop_e3fb63acb1c0213d33e5570b26edc928a770a02dae8317a04707641cdd803978 with PER leaving 3 subgoals.

The subproof is completed by applying L6.

The subproof is completed by applying L7.

The subproof is completed by applying L8.

■

Proofgold Proof