fact: Definition eq_ex2_rect_uncurried {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (R : u = v -> Type) (f : forall pqr : exists2 p : _ = _, _ & _, R (eq_ex2 u v (ex_proj1 pqr) (ex_proj2 pqr) (ex_proj3 pqr))) : forall p, R p := eq_ex2_rect R (fun p q r => f (ex_intro2 _ _ p q r)).
imports: Notations Ltac