fact: Definition ap_transport_Vp_idmap {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.
imports: Basics.Overture Basics.Tactics