proposition: Theorem CLL_cf_undec : undecidable CLL_cf_PROVABILITY.
proof: Proof. undec from EILL_undec; auto. Qed.
imports: Undecidability.Shared.Libs.DLW(utils_tac) Undecidability.Synthetic.Undecidability Undecidability.ILL(EILL ILL CLL ILL_undec EILL_CLL ILL_CLL)