proposition: Lemma cast_ext { X n m} (v1 v2 : Vector.t X n) (E1 E2 : n = m) : v1 = v2 -> cast v1 E1 = cast v2 E2.
proof: Proof. intros ->. destruct E1. cbn. now rewrite !cast_eq_refl. 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)