Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: nat_p x1.

Apply unknownprop_bfc870f6d786cc78805c5bf0f9864161d18f532f6daf7daf1d02f4a58dac06f9 with x0, ordsucc x1, λ x2 x3 . x3 = ordsucc (ordsucc (add_nat x0 x1)) leaving 2 subgoals.

Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with x1.

The subproof is completed by applying H0.

set y2 to be ordsucc (add_nat x0 (ordsucc x1))

set y3 to be ordsucc (ordsucc (add_nat x1 y2))

Claim L1: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2

Let x4 of type ι → ο be given.

Assume H1: x4 (ordsucc (ordsucc (add_nat y2 y3))).

set y5 to be λ x5 . x4

Apply unknownprop_bfc870f6d786cc78805c5bf0f9864161d18f532f6daf7daf1d02f4a58dac06f9 with y2, y3, λ x6 x7 . y5 (ordsucc x6) (ordsucc x7) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

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

Apply L1 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H2: x4 y3 y3.

The subproof is completed by applying H2.

■

Proofgold Proof