proposition: Lemma rew_sig {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 = exist (Q y) (rew H in proj1_sig u) (rew dependent H in proj2_sig u).
proof: Proof. destruct H, u; reflexivity. Defined.
imports: Notations Ltac Datatypes Logic