Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with λ x0 . or (x0 = 0) (∃ x1 . and (nat_p x1) (x0 = ordsucc x1)) leaving 2 subgoals.

Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with 0 = 0, ∃ x0 . and (nat_p x0) (0 = ordsucc x0).

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

Assume H0: x0 0 0.

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: or (x0 = 0) (∃ x1 . and (nat_p x1) (x0 = ordsucc x1)).

Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with ordsucc x0 = 0, ∃ x1 . and (nat_p x1) (ordsucc x0 = ordsucc x1).

Let x1 of type ο be given.

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

Apply H2 with x0.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with nat_p x0, ordsucc x0 = ordsucc x0 leaving 2 subgoals.

The subproof is completed by applying H0.

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

Assume H3: x2 (ordsucc x0) (ordsucc x0).

The subproof is completed by applying H3.

■

Proofgold Proof