proposition: Lemma Vapp_cast : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) n2' (e : n2 = n2'), Vapp v1 (Vcast v2 e) = Vcast (Vapp v1 v2) (Vapp_cast_aux n1 e).
proof: Proof. induction v1; simpl; intros. apply Vcast_pi. rewrite Vcast_cons, IHv1. f_equal. apply Vcast_pi. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)