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