proposition: Lemma cast_vec_pos { X n m} (v : Vector.t X n) (E : n = m) p : cast v E #> p = v #> Fin.cast p (eq_sym E).
proof: Proof. destruct E. cbn. now rewrite cast_eq_refl, fin_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)