fact: Definition equiv_moveL_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : q @ p^ = r <~> q = r @ p := Build_Equiv _ _ _ (isequiv_moveL_pM p q r).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics