proposition: Lemma Inb_true : forall x l, Inb x l = true -> In x l.
proof: Proof. induction l; simpl. intro. discr. case (eq_dec x a); auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)