proposition: Theorem ProperRelationalChoice: ∀ A B {eqA: Equiv A} {eqB: Equiv B} {equA: Equivalence eqA} {equB: Equivalence eqB} (R: A → B → Prop) (Rproper: Proper (equ ==> equ ==> iff) R) (Rfull: ∀ x, ∃ y, R x y), ∃ (R': A → B → Prop), (∀ x y, R' x y → R x y) ∧ Proper (equ ==> equ ==> iff) R' ∧ (∀ x, ∃ y, R' x y) ∧ ∀ x y y', R' x y → R' x y' → y ≌ y'.
proof: Proof. intros. specialize (setoid_choice A B eqA R equA) with (2 := Rfull) as F. clear Rfull. assert (H: ∀ (x x' : A) (y : B), eqA x x' → R x y → R x' y). { intros ? ? ? EQ. rewrite (Rproper _ _ EQ y y); [trivial | eapply equB]. } specialize (F H); clear H. destruct F as [f F]. exists (fun a b => eqB (f a) b). repeat split. * intros ? ? EQ. specialize (Rproper x x). red in Rproper. erewrite Rproper. + eapply F. + eapply equA. + destruct equB; apply Equivalence_Symmetric; assumption. * eapply F in H. rewrite H. destruct equB. intro; eapply Equivalence_Transitive; eassumption. * eapply F in H. rewrite H. destruct equB. intros; eapply Equivalence_Transitive. + eassumption. + apply Equivalence_Symmetric; assumption. * intros; eexists; eapply equB. * intros; red; destruct equB. eauto using Equivalence_Transitive, Equivalence_Symmetric. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)