proposition: Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop) (u : { p : P x & Q x p & R x p }) {y} (H : x = y) : rew [fun a => { p : P a & Q a p & R a p }] H in u = existT2 (Q y) (R y) (rew H in u.1) (rew dependent H in u.2) (rew dependent H in u.3).
proof: Proof. destruct H, u; reflexivity. Defined.
imports: Notations Ltac Datatypes Logic