proposition: Lemma Path_ind (P : forall x x0 : G, Path x x0 -> Type) (y : G) (x : G) (p : Path x y) : P y y (idp y) -> (forall (x z : G) (p : Path z y) (xz : x -- z), P z y p -> P x y (pcat (edgep xz) p)) -> P x y p.
proof: Proof. move => Hbase Hstep. case: p => [p pth_p]. elim: p x pth_p => [|z p IH] x A. - have ?: x = y. { exact: pathp_nil. } subst y. rewrite [Build_Path _](_ : _ = idp x) //. exact: val_inj. - move: {-}(A). rewrite pathp_cons => /andP [xz B2]. have -> : Build_Path A = (pcat (edgep xz) (Build_Path B2)) by exact: val_inj. apply: Hstep. exact: IH. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)