proposition: Lemma pos_left_inj {n m} p q : @pos_left n m p = @pos_left n m q -> p = q.
proof: Proof. induction p in q |- *; cbn in *. - eapply (Fin.caseS' q). + reflexivity. + clear q. cbn. congruence. - eapply (Fin.caseS' q). + cbn. congruence. + clear q. cbn. intros. f_equal. eapply IHp. now eapply pos_nxt_inj. 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)