fact: Definition eq_exist_l {A : Type} {P : A -> Prop} {u1 : A} {u2 : P u1} {v : { a : A | P a }} (p : u1 = proj1_sig v) (q : rew p in u2 = proj2_sig v) : exist _ u1 u2 = v := eq_sig (exist _ u1 u2) v p q.
imports: Notations Ltac Datatypes Logic