proposition: Lemma nth_replace_neq A: forall n p q, p <> q -> forall (v : t A n) a, nth (replace v q a) p = nth v p.
proof: Proof. intros n p q Hpq v a. induction v as [|b n v IH]; revert Hpq. - now apply Fin.case0. - apply (Fin.caseS' p); apply (Fin.caseS' q); [easy..|]. intros ???. apply IH. contradict Hpq. now f_equal. Qed.
imports: VectorDef PeanoNat Eqdep_dec