{A B C} (f : forall x, B x -> C) {g g' : forall x:A, B x} (p : g = g') a : apD10 (ap (fun h : forall x:A, B x => fun x => f x (h x)) p) a = ap (f a) (apD10 p a). Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.