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