proposition: Lemma nth_order_tl A: forall n k (v : t A (S n)) (H : k < n) (HS : S k < S n), nth_order (tl v) H = nth_order v HS.
proof: Proof. intros n; induction n; intros k v H HS. - inversion H. - rewrite (eta v). unfold nth_order; simpl. now rewrite (Fin.of_nat_ext H (proj2 (Nat.succ_lt_mono _ _) HS)). Qed.
imports: VectorDef PeanoNat Eqdep_dec