proposition: Lemma similar_ok : forall c1 c2, similar c1 c2 -> (c1 =i c2).
proof: Proof. move => c1 c2; rewrite /similar. move/eqP => h u. rewrite 2!canonize_mem. by rewrite h. 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)