proposition: Lemma Vapp_eq_intro : forall n1 (v1 v1' : vector A n1) n2 (v2 v2' : vector A n2), v1 = v1' -> v2 = v2' -> Vapp v1 v2 = Vapp v1' v2'.
proof: Proof. intros. rewrite H, H0. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)