proposition: Lemma inv_sim_step {s t'} : SSTS.step ssts (map enc s) t' -> exists t, t' = map enc t /\ SR2ab.step srs s t.
proof: Proof. move Hs': (map enc s) => s' Hs't'. case: Hs't' Hs' => u' v' a' b' c' d' H Hs. move: H. rewrite /ssts in_map_iff. move=> [[[a b]]] [c d] [[]] ? ? ? ?. subst. move=> H. exists (firstn (length u') s ++ c :: d :: skipn (length u' + 2) s). constructor. - rewrite map_app /= -firstn_map -skipn_map Hs. rewrite firstn_app (ltac:(lia) : length u' - length u' = 0) firstn_all. rewrite skipn_app (ltac:(lia) : length u' + 2 - length u' = 2) skipn_all2 /=; first by lia. by rewrite app_nil_r. - move: H => /SR2ab.stepI. apply; last done. apply: map_enc_inj. rewrite Hs map_app /= -firstn_map -skipn_map Hs. rewrite firstn_app (ltac:(lia) : length u' - length u' = 0) firstn_all. rewrite skipn_app (ltac:(lia) : length u' + 2 - length u' = 2) skipn_all2 /=; first by lia. by rewrite app_nil_r. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun