fact: Definition ap_lambda {A B C : Type} {x y : A} (p : x = y) (M : A -> B -> C) : ap (fun a b => M a b) p = path_arrow _ _ (fun b => ap (fun a => M a b) p).
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall