{A B} (p q : A = B) (r : q = p) (z : B) : ap (transport idmap q) (ap (fun s => transport idmap s^ z) r) @ ap (fun s => transport idmap s (p^ # z)) r @ transport_pV idmap p z = transport_pV idmap q z. Proof. by path_induction. Defined.
Require Import Basics.Overture Basics.Tactics.