fact: Variables (x : eill_vars) (Hvalid : forall n s, @ill_sequent_tps n s (map (fun c => !⦑c⦒) Σ ++ map £ Γ) (£ x) vec_zero).
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill)