proposition: Lemma nodup_incl_length : forall l l' : list A, nodup l -> incl l l' -> length l <= length l'.
proof: Proof. induction l; simpl; intros. apply Nat.le_0_l. apply Nat.le_trans with (S (length (remove eq_dec a l'))). apply le_n_S. apply IHl. tauto. apply incl_remove. tauto. apply incl_cons_l_incl with a. hyp. apply NatCompat.lt_le_S. apply In_length_remove. apply incl_cons_l_in with l. hyp. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)