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