proposition: Lemma nth_order_replace_eq A: forall n k (v : t A n) a (H1 : k < n) (H2 : k < n), nth_order (replace v (Fin.of_nat_lt H2) a) H1 = a.
proof: Proof. intros n k v a H1 H2. rewrite (Fin.of_nat_ext H2 H1). apply nth_replace_eq. Qed.
imports: VectorDef PeanoNat Eqdep_dec