proposition: Lemma Vapp_lcast_eq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p1 (h1 : n1=p1) (h2 : n1+n2=p1+n2), Vapp (Vcast v1 h1) v2 = Vcast (Vapp v1 v2) h2.
proof: Proof. induction v1; intros until p1; case p1; simpl; intros; try discr. repeat rewrite Vcast_refl; refl. rewrite !Vcast_cons. simpl. f_equal. apply IHv1. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)