proposition: Fact ndmm2_imsell_eq1 Σ : map (fun c => ![∞]⟬c⟭) Σ = ‼(map (fun c => (∞,⟬c⟭)) Σ).
proof: Proof. unfold imsell_lban; rewrite map_map; auto. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)