fact: Definition eq_exist_r {A : Type} {P : A -> Prop} {u : { a : A | P a }} {v1 : A} {v2 : P v1} (p : proj1_sig u = v1) (q : rew p in proj2_sig u = v2) : u = exist _ v1 v2 := eq_sig u (exist _ v1 v2) p q.
imports: Notations Ltac Datatypes Logic