proposition: Fact reduces_ireduces_iff : P ⪯ Q <-> inhabited (P ⪯ᵢ Q).
proof: Proof. split. + apply reduces_ireduces. + intros []; apply ireduces_reduces; auto. Qed.
imports: Undecidability.Synthetic(InformativeDefinitions DecidabilityFacts)