Apply add_nat_SR with u4, 0, λ x0 x1 . x1 = u5 leaving 2 subgoals.

The subproof is completed by applying nat_0.

set y0 to be ordsucc u4

Claim L0: ∀ x1 : ι → ο . x1 y0 ⟶ x1 (ordsucc (add_nat u4 0))

Let x1 of type ι → ο be given.

The subproof is completed by applying add_nat_0R with u4, λ x2 x3 . (λ x4 . x1) (ordsucc x2) (ordsucc x3).

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

Apply L0 with λ x2 . x1 x2 y0 ⟶ x1 y0 x2.

Assume H1: x1 y0 y0.

The subproof is completed by applying H1.

■

Proofgold Proof