proposition: Lemma forall_exists_coincide_unique_domain : forall A (P:A->Prop), (forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x)) -> (exists! x, P x).
proof: Proof. intros A P H. destruct (H P) as ((x & Hx & _),_); [trivial|]. exists x. split; [trivial|]. destruct (H (fun x'=>x=x')) as (_,Huniq). apply Huniq. exists x; auto. Qed.
imports: Notations Ltac