proposition: Lemma incl_shrink : forall l : list A, incl (shrink l) l.
proof: Proof. induction l; simpl; intros. apply incl_nil. destruct (In_dec eq_dec a (shrink l)). trans (shrink l). apply incl_cut. apply incl_tl. hyp. unfold incl. intros. simpl in H. simpl. case (eq_dec a a0); intro. subst a0. auto. right. apply IHl. destruct H. contr. exact H. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)