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