proposition: Fact ill_cll_has_bot_eq f : ill_has_bot f <-> cll_has_bot_zero_neg [f].
proof: Proof. split. + apply ill_cll_has_bot. + intros H. apply cll_ill_has_bot in H. now rewrite ill_cll_ill in H. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL)