fact: Definition ap_apply_l {A B : Type} {x y : A -> B} (p : x = y) (z : A) : ap (fun f => f z) p = ap10 p z := 1.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall