proposition: Lemma Vnth_tail : forall n (v : vector A (S n)) i (h : i < n), Vnth (Vtail v) h = Vnth v (NatCompat.lt_n_S h).
proof: Proof. intros. VSntac v. simpl. apply Vnth_eq. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)