proposition: Lemma regular_det (char : finType) L (w : word char): inhabited (regular L) -> (L w) \/ (~ L w).
proof: Proof. case. case => A ->. by case: (w \in dfa_lang A); [left|right]. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)