Let e, m and i be given.
Assume HiDom: i ∈ ordsucc (ordsucc m).
We prove the intermediate claim Hdef: swap_last_two e m = graph (ordsucc (ordsucc m)) (λj : set ⇒ if j = m then apply_fun e (ordsucc m) else if j = ordsucc m then apply_fun e m else apply_fun e j).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph (ordsucc (ordsucc m)) (λj : set ⇒ if j = m then apply_fun e (ordsucc m) else if j = ordsucc m then apply_fun e m else apply_fun e j) i HiDom) (from left to right).
Use reflexivity.
∎