proposition: Fact ireduces_transitive : P ⪯ᵢ Q -> Q ⪯ᵢ R -> P ⪯ᵢ R.
proof: Proof. unfold inf_reduces, reduction. intros (f & Hf) (g & Hg). exists (fun x => g (f x)). intro; rewrite Hf, Hg; tauto. Qed.
imports: Undecidability.Synthetic(InformativeDefinitions DecidabilityFacts)