We will prove TwoRamseyProp (ordsucc 2) (ordsucc 4) (ordsucc (ordsucc 12)).
rewrite the current goal using add_nat_8_4 (from right to left).
We will prove TwoRamseyProp (ordsucc 2) (ordsucc 4) (ordsucc (ordsucc (8 + 4))).
Apply TwoRamseyProp_bd 2 4 8 4 nat_8 nat_4 to the current goal.
We will prove TwoRamseyProp (ordsucc 2) 4 (ordsucc 8).
We will prove TwoRamseyProp 3 4 9.
An exact proof term for the current goal is TwoRamseyProp_3_4_9.
We will prove TwoRamseyProp 2 (ordsucc 4) (ordsucc 4).
We will prove TwoRamseyProp 2 5 5.
An exact proof term for the current goal is TwoRamseyProp_2 5.
∎