| pf |
|---|
Apply add_nat_SR with u51, 12, λ x0 x1 . x1 = u64 leaving 2 subgoals.
The subproof is completed by applying nat_12.
Apply add_nat_SR with u51, 11, λ x0 x1 . ordsucc x1 = u64 leaving 2 subgoals.
The subproof is completed by applying nat_11.
Apply add_nat_SR with u51, 10, λ x0 x1 . ordsucc (ordsucc x1) = u64 leaving 2 subgoals.
The subproof is completed by applying nat_10.
Apply add_nat_SR with u51, 9, λ x0 x1 . ordsucc (ordsucc (ordsucc x1)) = u64 leaving 2 subgoals.
The subproof is completed by applying nat_9.
■ |
|