Let F, e, i and n be given.
Assume HiDom: i ∈ n.
Assume HsiDom: ordsucc i ∈ n.
Assume HeFun: function_on e n F.
Let j be given.
Assume HjDom: j ∈ n.
We will prove apply_fun (swap_adjacent e i n) j ∈ F.
rewrite the current goal using (swap_adjacent_apply e i n j HjDom) (from left to right).
Apply (xm (j = i)) to the current goal.
Assume Hji: j = i.
rewrite the current goal using (If_i_1 (j = i) (apply_fun e (ordsucc i)) (if j = ordsucc i then apply_fun e i else apply_fun e j) Hji) (from left to right).
An exact proof term for the current goal is (HeFun (ordsucc i) HsiDom).
Assume Hnji: ¬ (j = i).
rewrite the current goal using (If_i_0 (j = i) (apply_fun e (ordsucc i)) (if j = ordsucc i then apply_fun e i else apply_fun e j) Hnji) (from left to right).
Apply (xm (j = ordsucc i)) to the current goal.
Assume Hjs: j = ordsucc i.
rewrite the current goal using (If_i_1 (j = ordsucc i) (apply_fun e i) (apply_fun e j) Hjs) (from left to right).
An exact proof term for the current goal is (HeFun i HiDom).
Assume Hnjs: ¬ (j = ordsucc i).
rewrite the current goal using (If_i_0 (j = ordsucc i) (apply_fun e i) (apply_fun e j) Hnjs) (from left to right).
An exact proof term for the current goal is (HeFun j HjDom).
∎