fact: Definition path_comp_assoc {i j k l} (x : Path (i,j)) (y : Path (j,k)) (z : Path (k,l)) : path_compose x (path_compose y z) = path_compose (path_compose x y) z.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple