fact: Definition eq_existT_r {A : Type} {P : A -> Type} {u : { a : A & P a }} {v1 : A} {v2 : P v1} (p : u.1 = v1) (q : rew p in u.2 = v2) : u = (v1; v2) := eq_sigT u (v1; v2) p q.
imports: Notations Ltac Datatypes Logic