proposition: Lemma subrel_pathp (T : finType) (e1 e2 : rel T) (x y : T) (p : seq T) : subrel e1 e2 -> @pathp (RelType e1) x y p -> @pathp (RelType e2) x y p.
proof: Proof. move => sub12. elim: p x => //= z p IHp x. rewrite !pathp_cons => /andP [A B]. apply/andP;split; [exact: sub12 | exact: IHp]. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)