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