proposition: Lemma star_eq l1 l2 : l1 =i l2 -> star l1 =i star l2.
proof: Proof. move => H1 w. apply/starP/starP; move => [] vv H3 H4; exists vv => //; erewrite eq_all; try eexact H3; move => x /=; by rewrite ?H1 // -?H1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)