proposition: Lemma sim_dec3 : forall x y, {sim3 x y}+{~sim3 x y}.
proof: Proof. case => [[a1 b1] s1] [[a2 b2] s2]. rewrite /sim3 /wsim /sim /=. case: (similar a1 a2). case: (similar b1 b2). by left; split. by right; case => [[]]. by right; case => [[]]. Defined.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)