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