Let F, e and m be given.
Assume HmNat: nat_p m.
Assume HeFun: function_on e (ordsucc (ordsucc m)) F.
Let j be given.
Assume HjDom: j ∈ ordsucc (ordsucc m).
We will prove apply_fun (swap_last_two e m) j ∈ F.
rewrite the current goal using (swap_last_two_apply e m j HjDom) (from left to right).
Apply (xm (j = m)) to the current goal.
Assume Hjm: j = m.
rewrite the current goal using (If_i_1 (j = m) (apply_fun e (ordsucc m)) (if j = ordsucc m then apply_fun e m else apply_fun e j) Hjm) (from left to right).
An exact proof term for the current goal is (HeFun (ordsucc m) (ordsuccI2 (ordsucc m))).
Assume Hnjm: ¬ (j = m).
rewrite the current goal using (If_i_0 (j = m) (apply_fun e (ordsucc m)) (if j = ordsucc m then apply_fun e m else apply_fun e j) Hnjm) (from left to right).
Apply (xm (j = ordsucc m)) to the current goal.
Assume HjS: j = ordsucc m.
rewrite the current goal using (If_i_1 (j = ordsucc m) (apply_fun e m) (apply_fun e j) HjS) (from left to right).
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)).
An exact proof term for the current goal is (HeFun m HmDom).
Assume HnjS: ¬ (j = ordsucc m).
rewrite the current goal using (If_i_0 (j = ordsucc m) (apply_fun e m) (apply_fun e j) HnjS) (from left to right).
An exact proof term for the current goal is (HeFun j HjDom).
∎