proposition: Theorem G_eill_correct : (Σ; Γ ⊦ u -> S_ill_restr (Σi++Γi) ui) /\ (S_ill_restr (Σi++Γi) ui -> S_ill_restr_wc (Σi++Γi) ui) /\ (S_ill_restr (Σi++Γi) ui -> S_ill (Σi++Γi) ui) /\ (S_ill_restr_wc (Σi++Γi) ui -> S_ill_wc (Σi++Γi) ui) /\ (S_ill (Σi++Γi) ui -> S_ill_wc (Σi++Γi) ui) /\ (S_ill_wc (Σi++Γi) ui -> Σ; Γ ⊦ u).
proof: Proof. msplit 5. + apply G_eill_sound. + apply S_ill_restr_restr_wc. + apply S_ill_restr_full. + apply S_ill_restr_full_wc. + apply S_ill_full_wc. + intro; apply G_eill_complete. intros; now apply ill_tps_sound. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill) Undecidability.ILL(CLL ill_cll schellinx)