fact: Definition eq_ex_rect {A : Prop} {P : A -> Prop} {u v : exists a : A, P a} (Q : u = v -> Type) (f : forall p q, Q (eq_ex u v p q)) : forall p, Q p := fun p => rew <- eq_ex_eta p in f _ _.
imports: Notations Ltac