fact: Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C }) (p : u.1 = v.1) (q : u.2 = v.2) (r : u.3 = v.3) : u = v := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
imports: Notations Ltac Datatypes Logic