proposition: Lemma map_sort : {morph map f : s1 / sort leT' s1 >-> sort leT s1}.
proof: Proof. move=> s; rewrite !sortE -[[::] in RHS]/(map (map f) [::]). elim: s [::] => /= [|x s ihs] ss; rewrite -/(map f [::]) -/(map f [:: _]); first by elim: ss [::] => //= x ss ihss ?; rewrite ihss map_merge. rewrite ihs -/(map f [:: x]); congr sort_rec1. by elim: ss [:: x] => {x s ihs} [|[|x s] ss ihss] //= ?; rewrite ihss map_merge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)