proposition: Lemma index_last_inj x y s : (x \in s) || (y \in s) -> index x s = indexlast y s -> x = y.
proof: Proof. elim: s=>[|k s IH] //=; rewrite !inE indexlast_cons !(eq_sym k). case: eqP=>[{k}<- _|_ /= S]; first by case: eqP=>//=. move: S; case/boolP: (y \in s)=>/=. - by rewrite andbF=>H _ []; apply: IH; rewrite H orbT. move=>Ny; rewrite orbF andbT. by case: eqP=>//; rewrite orbF=>_ H []; apply: IH; rewrite H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)