proposition: Theorem S_ill_cll_restr_equiv Γ A : Γ ⊢i A <-> ⟦Γ⟧ ⊢c [A]::∅.
proof: Proof. split; auto. intros H; apply S_cll_ill_restr in H; revert H. now rewrite ill_cll_ill_list, ill_cll_ill. Qed.
imports: List Permutation Arith Undecidability.ILL(ILL CLL ill_cll)