fact: Definition ap_uncurry {A B C} (f : A -> B -> C) {a a' : A} (p : a = a') {b b' : B} (q : b = b') : ap (uncurry f) (path_prod' p q) = ap011 f p q.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Decidable Types.Empty