proposition: Lemma Vin_dec : forall x n (xs : vector A n), {Vin x xs}+{~Vin x xs}.
proof: Proof. intro x. induction xs; simpl. right. fo. destruct (eq_dec h x). left. fo. destruct IHxs. left. fo. right. fo. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)