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