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