Let x0 of type ο be given.

Assume H0: ∀ x1 . (∃ x2 : ι → ι . ∃ x3 x4 x5 . ∃ x6 : ι → ι → ι → ι . MetaCat_nno_p PtdPred 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 PtdPred 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 PtdPred 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 PtdPred 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 PtdPred 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 PtdPred 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: ∀ x6 . PtdPred x6 ⟶ struct_p x6

...

Claim L7: PtdPred (pack_p 1 (λ x6 . True))

Apply unknownprop_2576d2815b46016e5e13a9989b4e9789629d83c56ed1c92a4cda0de077a20752 with 1, λ x6 . True.

Let x6 of type ο be given.

Assume H7: ∀ x7 . and (x7 ∈ 1) ((λ x8 . True) x7) ⟶ x6.

Apply H7 with 0.

Apply andI with 0 ∈ 1, (λ x7 . True) 0 leaving 2 subgoals.

The subproof is completed by applying In_0_1.

The subproof is completed by applying TrueI.

Claim L8: PtdPred (pack_p omega (λ x6 . True))

Apply unknownprop_2576d2815b46016e5e13a9989b4e9789629d83c56ed1c92a4cda0de077a20752 with omega, λ x6 . True.

Let x6 of type ο be given.

Assume H8: ∀ x7 . and (x7 ∈ omega) ((λ x8 . True) x7) ⟶ x6.

Apply H8 with 0.

Apply andI with 0 ∈ omega, (λ x7 . True) 0 leaving 2 subgoals.

Apply nat_p_omega with 0.

The subproof is completed by applying nat_0.

The subproof is completed by applying TrueI.

Apply unknownprop_87e4b92e864cd20cb66a704125e89f2601312b49a571aa5aeba3f0ceb096da6e with PtdPred 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