fact: Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v) : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v := rew dependent p in eq_refl.
imports: Notations Ltac Datatypes Logic