fact: Definition moveR_moveL_transport_p {A : Type} (P : A -> Type) {x y : A} (p : y = x) (u : P x) (v : P y) (q : transport P p^ u = v) : moveR_transport_V P p u v (moveL_transport_p P p u v q) = q.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics