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