proposition: Lemma sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} -> sorted leT s1 -> sorted leT s2 -> perm_eq s1 s2 -> s1 = s2.
proof: Proof. move=> /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_anti + + /[dup] s1s2. have /all_sigP[s1' ->] := allss s1. have /all_sigP[{s1s2}s2 ->] : all [in s1] s2 by rewrite -(perm_all _ s1s2). by rewrite !sorted_map => ss1' ss2 /(perm_map_inj val_inj)/(sorted_eq leT_tr)->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)