proposition: Lemma sub_in_path x s : all P (x :: s) -> path e x s -> path e' x s.
proof: Proof. by elim: s x => //= y s ihs x /and3P [? ? ?] /andP [/ee' -> //]; apply/ihs/andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)