proposition: Lemma star_id l : star (star l) =i star l.
proof: Proof. move => u. apply/starP/starP => [[vs h1 h2]|]. elim: vs u h1 h2 => [|hd tl Ih] u h1 h2; first by exists [::]. move: h1 => /= h1. case/andP: h1; case/andP => hhd1 hhd2 htl. case: (Ih (flatten tl)) => //= [xs x1 x2]. case/starP: hhd2 => hds j1 j2. exists (hds ++ xs); first by rewrite all_cat; apply/andP. by rewrite h2 j2 /= x2 flatten_cat. move => [hs h1 h2]. exists hs => //. apply/allP => x x1. move/allP: h1 => h1. case/andP: (h1 x x1) => /= h3 h4. rewrite h3 /=. apply/starP. exists [:: x] => /=; first by rewrite h3 h4. by rewrite cats0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)