proposition: Lemma nodup_midex_incl_length : eq_midex A -> forall l l', nodup l -> incl l l' -> length l <= length l'.
proof: Proof. intro em. induction l; simpl; intros. apply Nat.le_0_l. destruct (In_elim_right em a l'). apply H0. simpl. tauto. destruct H1. rewrite (proj1 H1), (length_app x (a::x0)). assert (length l <= length (x++x0)). apply IHl. tauto. unfold incl in *|-* . intros. apply in_or_app. destruct (em a0 a). subst a0. tauto. assert (In a0 x \/ In a0 (a::x0)). apply in_app_or. rewrite <- (proj1 H1). apply H0. simpl. tauto. simpl in H4. intuition. rewrite (length_app x x0) in H2. simpl. lia. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)