proposition: Lemma Vin_appr : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2), Vin x v2 -> Vin x (Vapp v1 v2).
proof: Proof. induction v1; simpl; intros. hyp. right. apply IHv1. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)