proposition: Lemma Vapp_rcast_eq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p2 (h1 : n2=p2) (h2 : n1+n2=n1+p2), Vapp v1 (Vcast v2 h1) = Vcast (Vapp v1 v2) h2.
proof: Proof. induction v1; simpl; intros. f_equal. apply eq_unique. rewrite Vcast_cons. f_equal. apply IHv1. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)