fact: Definition pointwise_paths_concat {A} {P : A -> Type} {f g h : forall x, P x} : pointwise_paths A P f g -> pointwise_paths A P g h -> pointwise_paths A P f h := fun p q x => p x @ q x.
imports: Basics.Notations Basics.Datatypes Basics.Logic