proposition: Lemma Inb_false : forall x l, Inb x l = false -> In x l -> False.
proof: Proof. induction l; simpl. intros. contr. case (eq_dec x a). intros. discr. intros. destruct H0; auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)