proposition: Lemma getPosition_nth (X:eqType) k (d :X) xs: NoDup xs -> k < length xs -> getPosition xs (nth k xs d) = k.
proof: Proof. induction xs in k|-*. now cbn. intros H1 H2. inv H1. cbn. destruct k. - decide _. all:easy. - decide _. + subst a. cbn in H2. edestruct H3. eapply nth_In. lia. + cbn in H2. rewrite IHxs. all:try easy;lia. Qed.