proposition: Lemma forall_exists_unique_domain_coincide : forall A (P:A->Prop), (exists! x, P x) -> forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x).
proof: Proof. intros A P (x & Hp & Huniq); split. - intro; exists x; auto. - intros (x0 & HPx0 & HQx0) x1 HPx1. assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto). destruct H. assumption. Qed.
imports: Notations Ltac