{A : Type} (B C : A -> Type) (D1 D2 : forall a, B a -> C a -> Type) (f : forall a b c, D1 a b c -> D2 a b c) {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D1 x1 y z) : f x2 (p # y) (p # z) (transportD2 B C D1 p y z w) = transportD2 B C D2 p y z (f x1 y z w). Proof. by induction p. Defined.
Require Import Basics.Overture Basics.Tactics.