proposition: Lemma sort_map_N_val n R : forall l : list (N n), sort (Rof R N_val) l -> sort R (map N_val l).
proof: Proof. induction l; intro h; simpl. apply nil_sort. inversion h; subst. apply cons_sort. tauto. apply lelistA_map_N_val. hyp. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil)