proposition: Lemma multi_step_repeat_sorI' {s t n x} : x = sb \/ x = sz -> multi_step srs ([so] ++ s) ([so] ++ t) -> multi_step srs ([so] ++ repeat x n ++ s) ([so] ++ repeat so n ++ t).
proof: Proof. move=> /multi_step_repeat_sorI H1 H2. apply: (rt_trans (y := ([so] ++ repeat so n ++ s))). - rewrite ?app_assoc. by apply: multi_step_apprI. - have ->: [so] = repeat so 1 by done. rewrite ?app_assoc -repeat_app. have ->: 1 + n = n + 1 by lia. rewrite repeat_app -?app_assoc. by apply: multi_step_applI. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun