proposition: Lemma pos_right_left {n m} p q : @pos_left n m p <> @pos_right n m q.
proof: Proof. induction n; cbn. - inversion p. - eapply (Fin.caseS' p). + cbn. congruence. + cbn. intros ? ? % pos_nxt_inj. firstorder. 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)