proposition: Lemma index_subseq (s1 s2 : seq A) a b : subseq s1 s2 -> uniq s2 -> a \in s1 -> b \in s1 -> index a s1 < index b s1 <-> index a s2 < index b s2.
proof: Proof. by case/subseqP=>m _ ->; apply: index_mask. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)