proposition: Theorem ill_cll_equiv Γ A : (forall f, In f (A::Γ) -> ~ ill_has_bot f) -> Γ ⊢i A <-> ⟦Γ⟧ ⊢c [A]::∅.
proof: Proof. intros H; split. + apply ill_cll_soundness. + intros H1. apply cll_ill_soundness in H1 as [ | [ ? | (f & ? & ?) ] ]; auto. * destruct (H A); simpl; auto. * destruct (H f); simpl; auto. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL ill_cll)