proposition: Lemma prop_5_2 p v : vec_pos v p = 0 -> Σ; vec_map_list v rx ⊦ ry p.
proof: Proof. rewrite <- (app_nil_r (_ _ rx)). intros H. apply g_eill_mono_Si with Σ0. unfold Σ; intros ? ?; apply in_or_app; left; auto. apply prop_5_2_rec; auto. apply in_geill_inc with (ry p) (ry p). right; apply in_or_app; right. apply in_map_iff. exists p; split; auto. apply pos_list_prop. apply in_geill_ax. 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)