proposition: Lemma Vin_app_cons : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2), Vin x (Vapp v1 (Vcons x v2)).
proof: Proof. induction v1; intros; simpl; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)