Let e, i and n be given.
Assume HiDom: i ∈ n.
We prove the intermediate claim Hsa: apply_fun (swap_adjacent e i n) i = if i = i then apply_fun e (ordsucc i) else if i = ordsucc i then apply_fun e i else apply_fun e i.
An exact proof term for the current goal is (swap_adjacent_apply e i n i HiDom).
rewrite the current goal using Hsa (from left to right).
We prove the intermediate claim Hrefl: i = i.
Use reflexivity.
rewrite the current goal using (If_i_1 (i = i) (apply_fun e (ordsucc i)) (if i = ordsucc i then apply_fun e i else apply_fun e i) Hrefl) (from left to right).
Use reflexivity.
∎