Let e, i and n be given.
Assume HsiDom: ordsucc i ∈ n.
We prove the intermediate claim Hsa: apply_fun (swap_adjacent e i n) (ordsucc i) = if ordsucc i = i then apply_fun e (ordsucc i) else if ordsucc i = ordsucc i then apply_fun e i else apply_fun e (ordsucc i).
An exact proof term for the current goal is (swap_adjacent_apply e i n (ordsucc i) HsiDom).
rewrite the current goal using Hsa (from left to right).
We prove the intermediate claim Hneq: ¬ (ordsucc i = i).
Assume Heq: ordsucc i = i.
We prove the intermediate claim Hii: i ∈ i.
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is (ordsuccI2 i).
An exact proof term for the current goal is ((In_irref i) Hii).
rewrite the current goal using (If_i_0 (ordsucc i = i) (apply_fun e (ordsucc i)) (if ordsucc i = ordsucc i then apply_fun e i else apply_fun e (ordsucc i)) Hneq) (from left to right).
We prove the intermediate claim Hrefl: ordsucc i = ordsucc i.
Use reflexivity.
rewrite the current goal using (If_i_1 (ordsucc i = ordsucc i) (apply_fun e i) (apply_fun e (ordsucc i)) Hrefl) (from left to right).
Use reflexivity.
∎