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