fact: Variable similar_congr_Conc : forall a b c d, similar a b -> similar c d -> similar (Conc a c) (Conc b d).
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)