proposition: Corollary G_eill_S_ill_restr : Σ; Γ ⊦ u <-> S_ill_restr (Σi++Γi) ui.
proof: Proof. solve with 1 3. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill) Undecidability.ILL(CLL ill_cll schellinx)