fact: Definition eq_sig_rect_uncurried {A P} {u v : { a : A | P a }} (Q : u = v -> Type) (f : forall pq : exists p : proj1_sig u = proj1_sig v, _, Q (eq_sig u v (ex_proj1 pq) (ex_proj2 pq))) : forall p, Q p := eq_sig_rect Q (fun p q => f (ex_intro _ p q)).
imports: Notations Ltac Datatypes Logic