proposition: Lemma injective_index (A: finType) (x1 x2 : A) : index x1 = index x2 -> x1 = x2.
proof: Proof. destruct (elem A) eqn:E. - hnf. intros. assert (x1 el elem A) by eauto using elem_spec. now rewrite E in H0. - clear E. intros E. apply (f_equal (fun y => nth y (elem A) e)) in E. now rewrite !index_nth in E. Qed.