proposition: Lemma multi_step_repeat_sorI {n x} : x = sb \/ x = sz -> multi_step srs ([so] ++ repeat x n) ([so] ++ repeat so n).
proof: Proof. move=> Hx. elim: n; first by apply: rt_refl. move=> n IH. apply: (rt_trans (y := ([so] ++ [so] ++ repeat x n))); last by apply: multi_step_applI. apply /rt_step /stepI_nil. move: Hx => [] ->; by eauto with in_srs_db nocore. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun