proposition: Lemma rew_existT_curried {A x} {P: A -> Type} {Q: {a & P a} -> Type} {y} {H: x = y} {u: P x} {v: Q (x; u)} {u': P y} {v': Q (y; u')} {Hu: rew H in u = u'} {Hv: rew (=H; Hu) in v = v'}: rew [fun x => {a: P x & Q (x; a)}] H in (u; v) = (u'; v').
proof: Proof. now destruct Hu, Hv, H. Qed.
imports: Bonak(Notation)