fact: Definition path_sigma {A : Type} {P : A -> Type} {u v : sigma A P} (p : u.1 = v.1) (q : rew p in u.2 = v.2) : u = v := match q in (_ = v2) return u = &(v.1 & v2) with | eq_refl => match p as p in (_ = v1) return u = &(v1 & subst p u.2) with | eq_refl => eq_refl end end.
imports: Equations DepElimDec