proposition: Theorem G_eill_complete : Σ; Γ ⊦ x.
proof: Proof. Proof using Hvalid. apply G_eill_complete_bound with (1 := w_surj), Hvalid. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill)