fact: Definition equiv_moveR_equiv_M `{IsEquiv A B f} (x : A) (y : B) : (x = f^-1 y) <~> (f x = y) := Build_Equiv _ _ (@moveR_equiv_M A B f _ x y) _.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics