proposition: Theorem G_eill_S_cll : Σ; Γ ⊦ u <-> S_cll (Σc++Γc) (uc::nil).
proof: Proof. split. + rewrite G_eill_S_ill. intros H. rewrite ill_cll_equiv in H; auto. eq goal H; f_equal. now rewrite map_app, !map_map. + intros H. apply G_eill_S_ill, ill_cll_equiv; auto. eq goal H; f_equal. now rewrite map_app, !map_map. Qed.
imports: List Permutation Arith Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.ILL(ILL EILL ill) Undecidability.ILL(CLL ill_cll schellinx)