Apply add_nat_SR with u6, u17, λ x0 x1 . x1 = u24 leaving 2 subgoals.

The subproof is completed by applying nat_17.

Apply add_nat_SR with u6, u16, λ x0 x1 . ordsucc x1 = u24 leaving 2 subgoals.

The subproof is completed by applying nat_16.

Apply add_nat_com with u6, u16, λ x0 x1 . ordsucc (ordsucc x1) = u24 leaving 3 subgoals.

The subproof is completed by applying nat_6.

The subproof is completed by applying nat_16.

Apply unknownprop_dd3938713573242af0c4fea8e90696a5a614e277ed0440a5717dd66ee9d68a70 with λ x0 x1 . ordsucc (ordsucc x1) = u24.

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

Assume H0: x0 24 u24.

The subproof is completed by applying H0.

■

Proofgold Proof