proposition: Corollary ra_mm_simulator_0 (f : recalg 0) : { m & { P : list (mm_instr (pos (S m))) | ex (⟦f⟧ vec_nil) <-> (1,P) // (1,vec_zero) ↓ } }.
proof: Proof. destruct (ra_mm_simulator f) as (m & P & HP). exists m, P; rewrite (HP vec_nil), vec_app_nil; tauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat pos vec sss) Undecidability.MinskyMachines(mm_defs) Undecidability.MuRec.Util(recalg ra_mm)