Proofgold Proof

pf
Apply add_nat_SR with u3, 0, λ x0 x1 . x1 = u4 leaving 2 subgoals. The subproof is completed by applying nat_0. Apply add_nat_0R with u3, λ x0 x1 . ordsucc x1 = u4. Let x0 of type ι → ι → ο be given. Assume H0: x0 (ordsucc u3) u4. The subproof is completed by applying H0. ■