proposition: Theorem rILL_rCLL_cf_PROVABILITY : rILL_cf_PROVABILITY ⪯ rCLL_cf_PROVABILITY.
proof: Proof. apply reduces_dependent; exists. intros (Γ,A). exists (⟦Γ⟧,[A]::nil). apply S_ill_cll_restr_equiv. Qed.
imports: List Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.ILL(ILL CLL ill ill_cll ill_cll_restr)