proposition: Lemma inverse_transport n : SSTS.multi_step ssts (repeat 0 (1+n)) (repeat 1 (1+n)) -> SR2ab.multi_step srs (repeat a0 (1+n)) (repeat b0 (1+n)).
proof: Proof. Proof using Ha0b0. rewrite repeat_a0 repeat_b0. move: (repeat a0 _) (repeat b0 _) => s t. move Hs': (map enc s) => s'. move Ht': (map enc t) => t' /(@clos_rt_rt1n_iff _ _) Hs't'. elim: Hs't' s t Hs' Ht'. - move=> ? s t *. subst. have -> : s = t by apply: map_enc_inj. by apply rt_refl. - move=> > IH1 _ IH2 *. subst. move: IH1 => /inv_sim_step [t] [? ?]. subst. apply /rt_trans; [apply: rt_step; by eassumption | by apply: IH2]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun