proposition: Lemma Vadd_app : forall p (v : vector A p) q (w : vector A q) x, Vadd (Vapp v w) x = Vcast (Vapp v (Vadd w x)) (Vadd_app_aux p q).
proof: Proof. induction v; simpl; intros q w x. rewrite Vcast_refl. refl. rewrite Vcast_cons, IHv. f_equal. apply Vcast_pi. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)