proposition: Lemma path_relI x s : path [rel x y | e x y && e' x y] x s = path e x s && path e' x s.
proof: Proof. by elim: s x => //= y s IHs x; rewrite andbACA IHs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)