proposition: Lemma ssim2_Plus_id : forall c : regular_expression bool, ssim2 (Plus c c) c.
proof: Proof. rewrite /ssim2 /similar => c /=. rewrite mkPlus_id => //. by apply wf_re_can. 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)