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