proposition: Lemma step2_det s' t1' t2' : sss_step (@mma_sss _) (1, P') s' t1' -> sss_step (@mma_sss _) (1, P') s' t2' -> t1' = t2'.
proof: Proof. apply: sss_step_fun. by apply: mma_sss_fun. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect