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