fact: Definition ex_proj2_of_ex2_eq {A : Prop} {P Q : A -> Prop} {u v : exists2 a : A, P a & Q a} (p : u = v) : rew ex_proj1_of_ex2_eq p in ex_proj2 u = ex_proj2 v := rew dependent p in eq_refl.
imports: Notations Ltac