proposition: Lemma rew_sigT {A x} {P: A -> Type} (Q: forall a, P a -> Type) (u: { p: P x & Q x p }) {y} (H: x = y) : rew [fun x => { p : P x & Q x p }] H in u = (rew H in u.1; rew dependent [fun x H => Q x (rew H in u.1)] H in u.2).
proof: Proof. now destruct H, u. Qed.
imports: Bonak(Notation)