Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι → ο be given.

Assume H1: x1 0.

Assume H2: ∀ x2 . nat_p x2 ⟶ x0 = ordsucc x2 ⟶ x1 (ordsucc x2).

Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with x0 = 0, ∃ x2 . and (nat_p x2) (x0 = ordsucc x2), x1 x0 leaving 3 subgoals.

Apply unknownprop_7be30b7cfc1f28933d3b9926f9200a8d420af1a2342269d520eb5a249c6f8c26 with x0.

The subproof is completed by applying H0.

Assume H3: x0 = 0.

Apply H3 with λ x2 x3 . x1 x3.

The subproof is completed by applying H1.

Assume H3: ∃ x2 . and (nat_p x2) (x0 = ordsucc x2).

Apply H3 with x1 x0.

Let x2 of type ι be given.

Assume H4: (λ x3 . and (nat_p x3) (x0 = ordsucc x3)) x2.

Apply andE with nat_p x2, x0 = ordsucc x2, x1 x0 leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H5: nat_p x2.

Assume H6: x0 = ordsucc x2.

Apply H6 with λ x3 x4 . x1 x4.

Apply H2 with x2 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

■

Proofgold Proof