proposition: Lemma Vlast_tail : forall n (v : vector A (S n)), Vlast (Vhead v) (Vtail v) = Vlast (Vhead v) v.
proof: Proof. intros n v. VSntac v. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)