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