proposition: Fact ill_cll_has_bot f : ill_has_bot f -> cll_has_bot_zero_neg [f].
proof: Proof. induction f as [ | [] | | [] ]; simpl; tauto. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL)