proposition: Lemma rew_ex2 {A' : Type} {x} {P : A' -> Prop} (Q R : forall a, P a -> Prop) (u : exists2 p : P x, Q x p & R x p) {y} (H : x = y) : rew [fun a => exists2 p : P a, Q a p & R a p] H in u = ex_intro2 (Q y) (R y) (rew H in ex_proj1 u) (rew dependent H in ex_proj2 u) (rew dependent H in ex_proj3 u).
proof: Proof. destruct H, u; reflexivity. Defined.
imports: Notations Ltac