fact: Definition eq_ex_intro_r {A : Prop} {P : A -> Prop} (u : exists a : A, P a) v1 v2 (p : ex_proj1 u = v1) (q : rew p in ex_proj2 u = v2) : u = ex_intro P v1 v2 := eq_ex u (ex_intro P v1 v2) p q.
imports: Notations Ltac