proposition: Theorem EILL_CLL_cf_PROVABILITY : EILL_PROVABILITY ⪯ CLL_cf_PROVABILITY.
proof: Proof. apply reduces_dependent; exists. intros ((Σ,Γ),u). exists ( map (fun c => cll_una cll_bang [⦑c⦒]) Σ ++ map cll_var Γ, cll_var u::nil). apply G_eill_S_cll. Qed.
imports: List Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.ILL(EILL ILL CLL ill eill ill_cll)