Let x0 of type ι → ο be given.
Assume H0: x0 1.
Let x1 of type ο be given.
Assume H2:
∀ x2 . (∃ x3 : ι → ι . ∃ x4 x5 x6 . ∃ x7 : ι → ι → ι → ι . MetaCat_nno_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) x2 x3 x4 x5 x6 x7) ⟶ x1.
Apply H2 with
1.
Let x2 of type ο be given.
Assume H3:
∀ x3 : ι → ι . (∃ x4 x5 x6 . ∃ x7 : ι → ι → ι → ι . MetaCat_nno_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 x3 x4 x5 x6 x7) ⟶ x2.
Apply H3 with
λ x3 . lam x3 (λ x4 . 0).
Let x3 of type ο be given.
Assume H4:
∀ x4 . (∃ x5 x6 . ∃ x7 : ι → ι → ι → ι . MetaCat_nno_p x0 HomSet (λ x8 . lam_id x8) (λ x8 x9 x10 x11 x12 . lam_comp x8 x11 x12) 1 (λ x8 . lam x8 (λ x9 . 0)) x4 x5 x6 x7) ⟶ x3.
Apply H4 with
omega.
Let x4 of type ο be given.
Apply H5 with
lam 1 (λ x5 . 0).
Let x5 of type ο be given.
Apply H6 with
lam omega (λ x6 . ordsucc x6).
Let x6 of type ο be given.
Apply H7 with
λ x7 x8 x9 . lam omega (λ x10 . nat_primrec (ap x8 0) (λ x11 x12 . ap x9 x12) x10).
Apply unknownprop_b6c6271c48298d19f3c93efd26efbc828f58047d76fdd16d468ddcd04fb28691 with
x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.