proposition: Lemma Vin_app : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2), Vin x (Vapp v1 v2) -> Vin x v1 \/ Vin x v2.
proof: Proof. induction v1; intros; simpl in * . auto. destruct H. auto. assert (Vin x v1 \/ Vin x v2). apply IHv1. exact H. destruct H0; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)