proposition: Theorem ndmm2_imsell_correct p x y : Σ //ₙ x ⊕ y ⊦ p <-> ⟬Σ,x,y⟭ ⊢ ⌊p⌋.
proof: Proof. Proof using Hi Hbi Hba Hb Hai Hab Ha. split; 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)