proposition: Lemma index_nth {F : finType} (x:F) y: nth (index x) (elem F) y = x.
proof: Proof. unfold index, elem, enum. destruct F as [[X E] [A all_A]];cbn. pose proof (getPosition_correct x A) as H. destruct Dec. auto. apply notInZero in n. now setoid_rewrite all_A in n. Qed.