fact: Definition eq_ex_intro_l {A : Prop} {P : A -> Prop} u1 u2 (v : exists a : A, P a) (p : u1 = ex_proj1 v) (q : rew p in u2 = ex_proj2 v) : ex_intro P u1 u2 = v := eq_ex (ex_intro P u1 u2) v p q.
imports: Notations Ltac