Let i be given.

Assume Hi.

Let p be given.

Assume Hp0 Hp1 Hp2.

Apply ordsuccE 2 i Hi to the current goal.

Assume Hil: i ∈ 2.

An exact proof term for the current goal is cases_2 i Hil p Hp0 Hp1.

Assume Hie: i = 2.

rewrite the current goal using Hie (from left to right).

An exact proof term for the current goal is Hp2.

∎