proposition: Lemma index_inj xs x y : x \in xs -> index x xs = index y xs -> x = y.
proof: Proof. elim: xs=>[|k xs IH] //=; rewrite inE eq_sym. case: eqP=>[->{k} _|_ /= S]; case: eqP=>// _ []; apply: IH S. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)