proposition: Lemma traverse_step s t vs : step s t -> step (traverse s vs) (traverse t vs).
proof: Proof. elim: vs s t; [done|]. move=> [[] [xs u]] vs IH s t ?. - apply: IH. by apply: stepAppL. - apply: IH. by apply: stepAppR. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun