Let e and m be given.
Assume HmNat: nat_p m.
We prove the intermediate claim HmDom: m ∈ ordsucc (ordsucc m).
An exact proof term for the current goal is (ordsuccI1 (ordsucc m) m (ordsuccI2 m)).
We prove the intermediate claim Happ: apply_fun (swap_last_two e m) m = if m = m then apply_fun e (ordsucc m) else if m = ordsucc m then apply_fun e m else apply_fun e m.
An exact proof term for the current goal is (swap_last_two_apply e m m HmDom).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hmm: m = m.
Use reflexivity.
rewrite the current goal using (If_i_1 (m = m) (apply_fun e (ordsucc m)) (if m = ordsucc m then apply_fun e m else apply_fun e m) Hmm) (from left to right).
Use reflexivity.
∎