proposition: Corollary eval_lang A i: regex.lang A@i ≡ dfa.lang A i.
proof: Proof. setoid_rewrite eval_lang. 2: apply is_nfa_nfa. now rewrite nfa_lang. Qed.
imports: positives comparisons kleene regex rmx sums matrix_ext prop normalisation