proposition: Lemma Vapp_rcast : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p2 (h1 : n2=p2), Vapp v1 (Vcast v2 h1) = Vcast (Vapp v1 v2) (plus_reg_l_inv n1 h1).
proof: Proof. intros. apply Vapp_rcast_eq. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)