fact: Fixpoint from_ill f := match f with | cll_var _ => True | cll_cst cll_bot => True | cll_cst cll_top => True | cll_cst cll_1 => True | cll_una cll_bang f => from_ill f | cll_bin cll_times f g => from_ill f /\ from_ill g | cll_bin cll_with f g => from_ill f /\ from_ill g | cll_bin cll_plus f g => from_ill f /\ from_ill g | cll_bin cll_limp f g => from_ill f /\ from_ill g | _ => False end.
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL)