proposition: Lemma multi_step_appI {srs u v s t} : multi_step srs s t -> multi_step srs (u ++ s ++ v) (u ++ t ++ v).
proof: Proof. elim; [| move=> *; by apply: rt_refl | move=> *; apply: rt_trans; by eassumption ]. move=> {}s {}t [] u' v' > ?. apply /rt_step /(stepI (u := u ++ u') (v := v' ++ v)); last by eassumption. all: by rewrite -?app_assoc. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun