fact: Definition eq_ex_intro2_l {A : Prop} {P Q : A -> Prop} u1 u2 u3 (v : exists2 a : A, P a & Q a) (p : u1 = ex_proj1 v) (q : rew p in u2 = ex_proj2 v) (r : rew p in u3 = ex_proj3 v) : ex_intro2 P Q u1 u2 u3 = v := eq_ex2 (ex_intro2 P Q u1 u2 u3) v p q r.
imports: Notations Ltac