proposition: Lemma subseq_path_in x s1 s2 : {in x :: s2 & &, transitive leT} -> subseq s1 s2 -> path x s2 -> path x s1.
proof: Proof. by move=> tr /subseqP [m _ ->]; apply/(path_mask_in tr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)