{A B C D} (f : A -> B -> C) (g : C -> D) {x x' y y'} (p : x = x') (q : y = y') : ap011 (fun x y => g (f x y)) p q = ap g (ap011 f p q). Proof. destruct p; simpl. apply ap_compose. Defined.
Require Import Basics.Overture Basics.Tactics.