fact: Definition eq_ex {A : Prop} {P : A -> Prop} (u v : exists a : A, P a) (p : ex_proj1 u = ex_proj1 v) (q : rew p in ex_proj2 u = ex_proj2 v) : u = v := eq_ex_uncurried u v (ex_intro _ p q).
imports: Notations Ltac