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