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