proposition: Lemma Vcast_cons n (v : vector A n) x p (hS : S n = S p) : Vcast (Vcons x v) hS = Vcons x (Vcast v (eq_add_S hS)).
proof: Proof. inversion hS. rewrite (eq_unique hS (f_equal S H0)). case H0. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)