proposition: Lemma ssim2_congr_Star : forall a b : bregexp, ssim2 a b -> ssim2 (Star a) (Star b).
proof: Proof. by rewrite /ssim2 /similar => s1 s2 heq /=; rewrite (eqP heq). Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)