Let m be given.

Assume Hm.

Assume IHm: (∀i ∈ m, f i = g i) → Pi_SNo f m = Pi_SNo g m.

Assume H1: ∀i ∈ ordsucc m, f i = g i.

We prove the intermediate claim L1: ∀i ∈ m, f i = g i.

Let i be given.

Assume Hi.

Apply H1 to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

We prove the intermediate claim L2: f m = g m.

Apply H1 to the current goal.

Apply ordsuccI2 to the current goal.

We will prove Pi_SNo f (ordsucc m) = Pi_SNo g (ordsucc m).

rewrite the current goal using Pi_SNo_S f m Hm (from left to right).

rewrite the current goal using Pi_SNo_S g m Hm (from left to right).

We will prove Pi_SNo f m * f m = Pi_SNo g m * g m.

Use f_equal.

An exact proof term for the current goal is IHm L1.

An exact proof term for the current goal is L2.