{A : Type} (B : A -> Type) (C1 C2 : forall a : A, B a -> Type) (f : forall a b, C1 a b -> C2 a b) {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C1 x1 y) : f x2 (p # y) (transportD B C1 p y z) = transportD B C2 p y (f x1 y z). Proof. by induction p. Defined.
Require Import Basics.Overture Basics.Tactics.