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