proposition: Lemma Vnth_cons_head : forall x n (v : vector A n) k (h : k < S n), k = 0 -> Vnth (Vcons x v) h = x.
proof: Proof. intros. subst k. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)