proposition: Lemma star_cat w1 w2 l : w1 \in l -> w2 \in (star l) -> w1 ++ w2 \in star l.
proof: Proof. case: w1 => [|a w1] // H1 /starP [vv Ha Hf]. apply/starP. by exists ((a::w1) :: vv); rewrite ?Hf //= H1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)