proposition: Lemma Vlast_nth : forall n (v : vector A (S n)) x (h : n < S n), Vlast x v = Vnth v h.
proof: Proof. induction n; intros v x h. VSntac v. simpl. generalize (Vtail v); intro w; VOtac. simpl. refl. VSntac v. simpl. apply IHn. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)