fact: Definition ap10_ap_postcompose {A B C} (f : B -> C) {g g' : A -> B} (p : g = g') a : ap10 (ap (fun h : A -> B => f o h) p) a = ap f (ap10 p a) := apD10_ap_postcompose (fun a => f) p a.
imports: Basics.Overture Basics.Tactics