proposition: Lemma index_subseq (T : eqType) x y (s1 s2 : seq T) : y \in s1 -> subseq s1 s2 -> uniq s2 -> index x s1 <= index y s1 -> index x s2 <= index y s2.
proof: Proof. move=> y_s1 sub_s1_s2 uniq_s2; have uniq_s1 := subseq_uniq sub_s1_s2 uniq_s2. rewrite -!mem2_index ?mem2E // => [?|]; last exact: (mem_subseq sub_s1_s2). exact: subseq_trans sub_s1_s2. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)