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