proposition: Lemma move_sb_right {p n} : p < state_bound -> multi_step srs ((sb' p) :: repeat sb n) ((repeat sb n) ++ [sb' p]).
proof: Proof. move=> Hp. elim: n; first by apply: rt_refl. move=> n IH /=. apply: rt_trans; [apply: rt_step | apply: (multi_step_applI (u := [sb])); exact: IH]. apply: stepI_nil. by eauto with in_srs_db nocore. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun