fact: Fixpoint ill_cll f := match f with | ill_var v => cll_var v | ill_cst ill_bot => cll_cst cll_bot | ill_cst ill_top => cll_cst cll_top | ill_cst ill_1 => cll_cst cll_1 | ill_ban f => cll_una cll_bang [f] | ill_bin ill_times f g => cll_bin cll_times [f] [g] | ill_bin ill_with f g => cll_bin cll_with [f] [g] | ill_bin ill_plus f g => cll_bin cll_plus [f] [g] | ill_bin ill_limp f g => cll_bin cll_limp [f] [g] end where "[ f ]" := (ill_cll f).
imports: List Permutation Undecidability.Shared.Libs.DLW(utils) Undecidability.ILL(ILL CLL)