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