proposition: Corollary satisfies_dec I s : decidable (satisfies I s).
proof: Proof. apply: dec_iff (vec_of_valP I s). exact: decP (nfa_of_form_correct _ _). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)