{A B} {P Q : A -> B -> Type} {a1 a2 : A} {b1 b2 : B} (p : a1 = a2) (q : b1 = b2) (f : forall {a b}, P a b -> Q a b) (x : P a1 b1) : f (transport011 P p q x) = transport011 Q p q (f x). Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.