proposition: Lemma irr_sorted_eq_in s1 s2 : {in s1 & &, transitive leT} -> {in s1, irreflexive leT} -> sorted leT s1 -> sorted leT s2 -> s1 =i s2 -> s1 = s2.
proof: Proof. move=> /in3_sig leT_tr /in1_sig leT_irr + + /[dup] s1s2. have /all_sigP[s1' ->] := allss s1. have /all_sigP[s2' ->] : all [in s1] s2 by rewrite -(eq_all_r s1s2). rewrite !sorted_map => ss1' ss2' {}s1s2; congr map. by apply: (irr_sorted_eq leT_tr) => // x; rewrite -!(mem_map val_inj). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)