fact: Definition eq_ex_rect_uncurried {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (Q : u = v -> Type) (f : forall pq, Q (eq_ex u v (ex_proj1 pq) (ex_proj2 pq))) : forall p, Q p := eq_ex_rect Q (fun p q => f (ex_intro _ p q)).
imports: Notations Ltac