proposition: Theorem uniq_mklist: forall m, ulist (mklist m).
proof: Proof. intros m; elim m; simpl; auto; clear m. intros m H; constructor; auto. intros H1; absurd (m < m)%nat; auto with arith. apply mklist_lt; auto. Qed.
imports: ZArith Znumtheory Eqdep_dec List Lia UList