Let i be given.

Assume Hi.

Let p be given.

Assume Hp0 Hp1.

Apply ordsuccE 1 i Hi to the current goal.

Assume Hil: i ∈ 1.

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

Assume Hie: i = 1.

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

An exact proof term for the current goal is Hp1.

∎