proposition: Lemma path_compose_spec : ∀ {i j k l : I} (x : g (i,j)) (xs : Path (j,k)) (ys : Path (k,l)), path_compose (x :-: xs) ys = x :-: path_compose xs ys.
proof: Proof. intros. dependent destruction xs; dependent destruction ys; reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple