proposition: Lemma Halt_MM_iff P : Halt_MM P <-> MM_HALTING P.
proof: Proof. destruct P as (n & P & v); cbn. split. - intros (c' & v' & H % eval_iff). eexists. eauto. - intros [(c', v') H % eval_iff]. eauto. Qed.
imports: Coq(List Lia) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) Undecidability.MinskyMachines.MM