proposition: Theorem G_eill_mm i v : P // (i,v) ->> (k,vec_zero) <-> Σ; vec_map_list v rx ⊦ q i.
proof: Proof. Proof using Hk. split. + apply lemma_5_3. + now apply lemma_5_5. Qed.
imports: List Permutation Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs mm_utils) Undecidability.ILL(ILL EILL ill eill)