proposition: Corollary mso_dec s : decidable (exists I, satisfies I s).
proof: Proof. pose n := bound s. case: (nfa_inhabP (nfa_of_form n s)) => A;[left|right]. - case: A => w /(@nfa_of_form_correct n) Hw. by exists (I_of w). - move => [I sat_I_s]. apply A. exists (vec_of_val I n). apply/nfa_of_form_correct. by rewrite /vec_lang -vec_of_valP. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)