fact: Definition path_arrow_pp {A B : Type} (f g h : A -> B) (p : f == g) (q : g == h) : path_arrow f h (fun x => p x @ q x) = path_arrow f g p @ path_arrow g h q := path_forall_pp f g h p q.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall