proposition: Lemma replace_replace_eq A: forall n p (v : t A n) a b, replace (replace v p a) p b = replace v p b.
proof: Proof. intros n p v a b. induction p as [|? p IHp]; rewrite (eta v); simpl; [reflexivity|]. now rewrite IHp. Qed.
imports: VectorDef PeanoNat Eqdep_dec