proposition: Lemma pcatSE (x y z : G) (p : Path x y) (q : Path y z) : pcatS (PathS p) (PathS q) = PathS (pcat p q).
proof: Proof. rewrite /pcatS /=. case: {-}_ /altP => [E|]; last by rewrite eqxx. rewrite /castL. by rewrite (eq_irrelevance E erefl). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)