proposition: Lemma getPosition_correct {E: eqType} (x:E) A: if Dec (x el A) then forall z, (nth (getPosition A x) A z) = x else getPosition A x = |A |.
proof: Proof. induction A;cbn. - repeat destruct Dec;tauto. - repeat destruct Dec;intuition; congruence. Qed.