{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.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.