Apply add_nat_SR with u6, u5, λ x0 x1 . x1 = u12 leaving 2 subgoals.

The subproof is completed by applying nat_5.

Apply add_nat_SR with u6, u4, λ x0 x1 . ordsucc x1 = u12 leaving 2 subgoals.

The subproof is completed by applying nat_4.

Apply unknownprop_bb0cce2a8a891fc83c2d273bca3870e6d95b58f7c38b76aa14bb34832a6eb7db with λ x0 x1 . ordsucc (ordsucc x1) = u12.

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

Assume H0: x0 12 u12.

The subproof is completed by applying H0.

■

Proofgold Proof