proposition: Lemma vec_of_list_cons : forall a l, vec_of_list (a :: l) = Vcons a (vec_of_list l).
proof: Proof. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)