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