{A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f x)) : transport (fun x => P (f x)) p z = transport P (ap f p) z. Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.