{A B C} (f : forall (a:A), B a -> C a) {x x'} (p : x = x') {y y'} (q : p # y = y') : transport C p (f x y) = f x' y'. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.