proposition: Lemma subseq_rem x : {homo rem x : s1 s2 / @subseq T s1 s2}.
proof: Proof. move=> s1 s2; elim: s2 s1 => [|x2 s2 IHs2] [|x1 s1]; rewrite ?sub0seq //=. have [->|_] := eqVneq x1 x2; first by case: eqP => //= _ /IHs2; rewrite eqxx. move=> /IHs2/subseq_trans->//. by have [->|_] := eqVneq x x2; [apply: rem_subseq|apply: subseq_cons]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)