proposition: Lemma Vapp_assoc : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) n3 (v3 : vector A n3), Vapp (Vapp v1 v2) v3 = Vcast (Vapp v1 (Vapp v2 v3)) (Nat.add_assoc n1 n2 n3).
proof: Proof. intros. apply Vapp_assoc_eq. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)