proposition: Fact cll_ill_has_bot f : cll_has_bot_zero_neg f -> ill_has_bot ⟨f⟩.
proof: Proof. induction f as [ | [] | [] | [] ]; simpl; try tauto. all: intros []; auto; discriminate. Qed.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL)