{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. Proof. by destruct e, p. Defined.
Require Import Basics.Overture Basics.Tactics.