fact: Definition moveL_transport_p_V {A : Type} (P : A -> Type) {x y : A} (p : y = x) (u : P x) (v : P y) (q : p^ # u = v) : (moveL_transport_p P p u v q)^ = moveR_transport_p P p v u q^.
imports: Basics.Overture Basics.Tactics