proposition: Lemma sim_step {s t} : SR2ab.step srs s t -> SSTS.step ssts (map enc s) (map enc t).
proof: Proof. case => > ?. rewrite ?map_app /=. apply: step_intro. rewrite /ssts in_map_iff. eexists. by constructor; last by eassumption. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun