proposition: Lemma multi_step_applI {srs u s t} : multi_step srs s t -> multi_step srs (u ++ s) (u ++ t).
proof: Proof. move=> /multi_step_appI => /(_ u []). by rewrite ?app_nil_r. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun