fact: Definition dpath_path_l {A : Type} {x1 x2 y : A} (p : x1 = x2) (q : x1 = y) (r : x2 = y) : q = p @ r <~> transport (fun x => x = y) p q = r.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics