proposition: Lemma vec_list_inj {X n} (v w : Vector.t X n) : vec_list v = vec_list w -> v = w.
proof: Proof. induction v in w |- *. - pattern w. revert w. eapply Vector.case0. reflexivity. - eapply (Vector.caseS' w). clear w. intros y w. cbn. intros [= ->]. f_equal. eauto. 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)