proposition: Lemma length_shrink : forall l l' : list A, incl l l' -> length (shrink l) <= length l'.
proof: Proof. intros. apply nodup_midex_incl_length. exact (eq_dec_midex eq_dec). apply nodup_shrink. trans l. apply incl_shrink. hyp. Qed.
imports: Coq(PeanoNat) CoLoR(ListUtil ListNodup LogicUtil RelMidex)