proposition: Lemma ssim2_congr_And : forall a b c d : bregexp, ssim2 a b -> ssim2 c d -> ssim2 (And a c) (And b d).
proof: Proof. rewrite /ssim2 /similar => s1 s2 s3 s4 heq1 heq2 /=. by rewrite (eqP heq1) (eqP heq2). 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)