proposition: Lemma transport n : SR2ab.multi_step srs (repeat a0 (1+n)) (repeat b0 (1+n)) -> SSTS.multi_step ssts (repeat 0 (1+n)) (repeat 1 (1+n)).
proof: Proof. Proof using Ha0b0. rewrite repeat_a0 repeat_b0. move: (repeat a0 _) (repeat b0 _) => s t. elim. - move=> > ?. apply: rt_step. by apply: sim_step. - move=> *. by apply rt_refl. - move=> *. apply: rt_trans; by eassumption. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun