proposition: Fact mm_erase_progress i e : e⇢zero = 0 -> exists e', e' ⋈ e⦃dst⇠0⦄ /\ (i,mm_erase i) // (i,e) -+> (2+i,e').
proof: Proof. Proof using Hdz. intros H1. destruct mm_erase_spec with (e := e) (i := i) (x := e⇢dst) as (e' & H3 & H4); auto. exists e'; split; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)