Claim L0: (λ x0 . λ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 (x1 x2) = x1 x2) 1 (λ x0 . 0)

Let x0 of type ι be given.

Assume H0: x0 ∈ 1.

...

Claim L1: (λ x0 . λ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 (x1 x2) = x1 x2) omega (λ x0 . x0)

Let x0 of type ι be given.

Assume H1: x0 ∈ omega.

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

Assume H2: x1 x0 x0.

The subproof is completed by applying H2.

Let x0 of type ο be given.

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

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

Let x1 of type ο be given.

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

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

Let x2 of type ο be given.

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

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

Let x3 of type ο be given.

Assume H5: ∀ x4 . (∃ x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p 9f253.. 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 H5 with lam 1 (λ x4 . 0).

Let x4 of type ο be given.

Assume H6: ∀ x5 . (∃ x6 : ι → ι → ι → ι . MetaCat_nno_p 9f253.. 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 H6 with lam omega (λ x5 . ordsucc x5).

Let x5 of type ο be given.

Assume H7: ∀ x6 : ι → ι → ι → ι . MetaCat_nno_p 9f253.. 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 H7 with λ x6 x7 x8 . lam omega (λ x9 . nat_primrec (ap x7 0) (λ x10 x11 . ap x8 x11) x9).

Apply unknownprop_1897dd9d62036e24b5a15a6305884877d2b2984b6fa2f5de30c61ce53aecce82 with λ x6 . λ x7 : ι → ι . ∀ x8 . x8 ∈ x6 ⟶ x7 (x7 x8) = x7 x8 leaving 3 subgoals.

The subproof is completed by applying unknownprop_170570cd9c8bbfca7e90abaab69c5d65b36e383209d6e68011d09548573ef745.

The subproof is completed by applying L0.

The subproof is completed by applying L1.

■

Proofgold Proof