proposition: Lemma Inb_incl : forall x l l', l [= l' -> Inb x l = true -> Inb x l' = true.
proof: Proof. intros. apply Inb_intro. apply H. apply Inb_true. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)