proposition: Fact reduces_dependent : P ⪯ Q <-> inhabited (forall x, { y | P x <-> Q y }).
proof: Proof. constructor. - intros [f Hf]. constructor. intros x. now exists (f x). - intros [f]. exists (fun x => proj1_sig (f x)). intros x. exact (proj2_sig (f x)). Qed.
imports: Undecidability.Synthetic.Definitions