proposition: Lemma subseqP s1 s2 : reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).
proof: Proof. elim: s2 s1 => [|y s2 IHs2] [|x s1]. - by left; exists [::]. - by right=> -[m /eqP/nilP->]. - by left; exists (nseq (size s2).+1 false); rewrite ?size_nseq //= mask_false. apply: {IHs2}(iffP (IHs2 _)) => [] [m sz_m def_s1]. by exists ((x == y) :: m); rewrite /= ?sz_m // -def_s1; case: eqP => // ->. case: eqP => [_ | ne_xy]; last first. by case: m def_s1 sz_m => [|[] m] //; [case | move=> -> [<-]; exists m]. pose i := index true m; have def_m_i: take i m = nseq (size (take i m)) false. apply/all_pred1P; apply/(all_nthP true) => j. rewrite size_take ltnNge geq_min negb_or -ltnNge => /andP[lt_j_i _]. rewrite nth_take //= -negb_add addbF -addbT -negb_eqb. by rewrite [_ == _](before_find _ lt_j_i). have lt_i_m: i < size m. rewrite ltnNge; apply/negP=> le_m_i; rewrite take_oversize // in def_m_i. by rewrite def_m_i mask_false in def_s1. rewrite size_take lt_i_m in def_m_i. exists (take i m ++ drop i.+1 m). rewrite size_cat size_take size_drop lt_i_m. by rewrite sz_m in lt_i_m *; rewrite subnKC. rewrite {s1 def_s1}[s1](congr1 behead def_s1). rewrite -[s2](cat_take_drop i) -[m in LHS](cat_take_drop i) {}def_m_i -cat_cons. have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m. rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=. by rewrite (drop_nth true) // nth_index -?index_mem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)