proposition: Lemma Σ_zero c : In c Σ -> [[ ⦑c⦒ ]] vec_zero.
proof: Proof. Proof using Hk. intros H; apply in_app_or in H as []; auto. 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)