proposition: Lemma lelistA_map_N_val n R (a : N n) : forall l, lelistA (Rof R N_val) a l -> lelistA R a (map N_val l).
proof: Proof. induction l; intro h; simpl. apply nil_leA. inversion h; subst. apply cons_leA; auto. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil) CoLoR(SortUtil RelUtil)