{A : Type} {x y : A} (p : x = y) (q : y = x) : IsEquiv (moveL_V1 p q). Proof. destruct q. apply isequiv_concat_l. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics.