proposition: Theorem ill_cll_soundness Γ A : Γ ⊢i A -> ⟦Γ⟧ ⊢c [A]::∅.
proof: Proof. induction 1; simpl in *. + apply in_cll_ax. + apply (@in_cll_perm ⟦Γ⟧ ([A]::nil)); auto. + rewrite map_app. now apply in_cll_limp_l with (Δ := ∅) (Δ' := _::_). + now apply in_cll_limp_r with (Δ := ∅). + now apply in_cll_with_l1. + now apply in_cll_with_l2. + now apply in_cll_with_r with (Δ := ∅). + now apply in_cll_bang_l. + rewrite ill_cll_lbang in *. now apply in_cll_bang_r with (Δ := ∅). + now apply in_cll_weak_l. + now apply in_cll_cntr_l. + now apply in_cll_times_l. + rewrite map_app. now apply in_cll_times_r with (Δ := ∅) (Δ' := ∅). + now apply in_cll_plus_l. + now apply in_cll_plus_r1. + now apply in_cll_plus_r2. + apply in_cll_bot_l. + apply in_cll_top_r. + now apply in_cll_unit_l. + apply in_cll_unit_r. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL ill_cll)