Let i be given.

Assume Hi.

Let p be given.

Assume Hp0.

Apply ordsuccE 0 i Hi to the current goal.

Assume Hil: i ∈ 0.

Apply EmptyE i Hil to the current goal.

Assume Hie: i = 0.

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

An exact proof term for the current goal is Hp0.

∎