fact: Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a }) (pqr : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }) : u = v.
imports: Notations Ltac Datatypes Logic