{A : Type} {B : A -> Type} {P : forall a : A, B a -> Type} (f g : forall a b, P a b) : (forall x y, f x y = g x y) -> f = g := equiv_path_forall11 f g.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids