proposition: Lemma ssim2_PlusA : forall c1 c2 c3 : regular_expression bool, ssim2 (Plus (Plus c1 c2) c3) (Plus c1 (Plus c2 c3)).
proof: Proof. rewrite /ssim2 /similar => c d e /=. rewrite mkPlusA => //; 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)