proposition: Lemma incl_select : forall l, select l [= l.
proof: Proof. induction l; simpl. fo. destruct (f_dec a). apply cons_incl. refl. hyp. apply incl_tl. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)