proposition: Lemma Inb_elim : forall x l, ~In x l -> Inb x l = false.
proof: Proof. induction l; simpl; intros. refl. case (eq_dec x a). intro. subst x. intuition. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)