proposition: Lemma pos_right_inj {n m} p q : @pos_right n m p = @pos_right n m q -> p = q.
proof: Proof. induction n in p, q |- *; cbn in *. - eauto. - intros. eapply IHn, pos_nxt_inj, H. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)