proposition: Lemma sorted_subseq_inP s1 s2 : {in s2 & &, transitive leT} -> {in s2, irreflexive leT} -> sorted leT s1 -> sorted leT s2 -> reflect {subset s1 <= s2} (subseq s1 s2).
proof: Proof. move=> leT_tr leT_irr ss1 ss2; apply (iffP idP); first exact: mem_subseq. move: leT_tr leT_irr ss1 ss2 => /in3_sig leT_tr /in1_sig leT_irr . have /all_sigP[s2' ->] := allss s2 => + + /[dup] subs12. have /all_sigP[{subs12}s1 ->] : all (mem s2) s1. by apply/allP => i /subs12 /mapP[[j /= j_in_s2 _ ->{i}]]. rewrite !sorted_map => ss1 ss2' subs12. apply/map_subseq/(sorted_subseqP leT_tr leT_irr ss1 ss2'). by move=> i /(map_f sval) /subs12 /mapP[j j_in_s2'] /val_inj->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted