proposition: Lemma nth_order_ext A: forall n k (v : t A n) (H1 H2 : k < n), nth_order v H1 = nth_order v H2.
proof: Proof. intros n k v H1 H2; unfold nth_order. now rewrite (Fin.of_nat_ext H1 H2). Qed.
imports: VectorDef PeanoNat Eqdep_dec