fact: Definition ap_transport_transport_pV {A} (P : A -> Type) {x y : A} (p : x = y) (u : P x) (v : P y) (e : transport P p u = v) : ap (transport P p) (moveL_transport_V P p u v e) @ transport_pV P p v = e.
imports: Basics.Overture Basics.Tactics