proposition: Lemma starP : forall {l v}, reflect (exists2 vv, all [predD l & eps] vv & v = flatten vv) (v \in star l).
proof: Proof. move=> l v; elim: {v}_.+1 {-2}v (ltnSn (size v)) => // n IHn [|x v] /= le_v_n. by left; exists [::]. apply: (iffP concP) => [[u] [v'] [def_v [Lxu starLv']] | [[|[|y u] vv] //=]]. case/IHn: starLv' => [|vv lvv def_v']. by rewrite -ltnS (leq_trans _ le_v_n) // def_v size_cat !ltnS leq_addl. by exists ((x :: u) :: vv); [exact/andP | rewrite def_v def_v']. case/andP=> lyu lvv [def_x def_v]; exists u, (flatten vv). subst; do 2![split=>//]. apply/IHn; last by exists vv. by rewrite -ltnS (leq_trans _ le_v_n) // size_cat !ltnS leq_addl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)