{A : Type} (P : A -> Type) {x y : A} (p : y = x) (u : P x) (v : P y) (q : u = p # v) : (moveR_transport_V P p u v q)^ = moveL_transport_V P p v u q^. Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.