fact: Definition path_forall11 {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.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)