proposition: Corollary ill_tps_Σ_zero : ill_tps_list s (map (fun c => !⦑c⦒) Σ) vec_zero.
proof: Proof. Proof using Hk. generalize Σ Σ_zero; intros S. induction S as [ | A S IHS ]; intros HS. + simpl; auto. + simpl; exists vec_zero, vec_zero; repeat split; auto. * rew vec. * apply HS; left; auto. * apply IHS; intros; apply HS; right; 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)