{A B C} (f : A -> B -> C) {x x' x'' y y' y''} (p : x = x') (p' : x' = x'') (q : y = y') (q' : y' = y'') : ap011 f (p @ p') (q @ q') = ap011 f p q @ ap011 f p' q'. Proof. destruct p, p'. apply ap_pp. Defined.
Require Import Basics.Overture Basics.Tactics.