fact: Definition eq_ex2_uncurried {A : Prop} {P Q : A -> Prop} (u v : exists2 a : A, P a & Q a) (pqr : exists2 p : ex_proj1 u = ex_proj1 v, rew p in ex_proj2 u = ex_proj2 v & rew p in ex_proj3 u = ex_proj3 v) : u = v.
imports: Notations Ltac