proposition: Lemma Schellinx_observation Γ : Γ ⊢c ∅ -> exists f, In f Γ /\ cll_has_bot_zero_neg f.
proof: Proof. intros; now apply schellinx_rec with (2 := eq_refl). Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL ill_cll)