fact: Definition ap_lambdaD {A B : Type} {C : B -> Type} {x y : A} (p : x = y) (M : forall a b, C b) : ap (fun a b => M a b) p = path_forall _ _ (fun b => ap (fun a => M a b) p).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)