proposition: Lemma wsim_dec : forall (a b : bword), {wsim a b}+{~wsim a b}.
proof: Proof. rewrite /wsim => a b. by left. Defined.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)