proposition: Theorem S_ill_cll_restr Γ A : Γ ⊢i A -> ⟦Γ⟧ ⊢c [A]::∅.
proof: Proof. induction 1. + apply in_cll1_ax. + apply (@in_cll1_perm ⟦Γ⟧ ([A]::nil)); auto. + simpl; rewrite map_app; now apply in_cll1_limp_l with (Δ := ∅) (Δ' := _::_). + now apply in_cll1_limp_r with (Δ := ∅). + now apply in_cll1_with_l1. + now apply in_cll1_with_l2. + now apply in_cll1_with_r with (Δ := ∅). + now apply in_cll1_bang_l. + rewrite ill_cll_lbang in *; simpl; now apply in_cll1_bang_r. + now apply in_cll1_weak_l. + now apply in_cll1_cntr_l. Qed.
imports: List Permutation Arith Undecidability.ILL(ILL CLL ill_cll)