proposition: Lemma weak_coincidence I I' s : (forall X, I X =i I' X) -> satisfies I s -> satisfies I' s.
proof: Proof. move => H. by rewrite (@coincidence I I' s). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)