proposition: Fact ireduces_dependent : (P ⪯ᵢ Q -> forall x, { y | P x <-> Q y }) * ((forall x, { y | P x <-> Q y }) -> P ⪯ᵢ Q).
proof: Proof. unfold inf_reduces, reduction. split. + intros (f & Hf). intros x; exists (f x); auto. + intros f. exists (fun x => proj1_sig (f x)). intros; apply (proj2_sig (f x)). Qed.
imports: Undecidability.Synthetic(InformativeDefinitions DecidabilityFacts)