proposition: Lemma Inb_correct : forall x l, In x l <-> Inb x l = true.
proof: Proof. intuition. apply Inb_intro. hyp. apply Inb_true. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)