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