proposition: Theorem eval_lang n u M v (H: is_nfa (@mk n u M v)): regex.lang (mx_scal (u ⋅ M^* ⋅ v)) ≡ lang M v u.
proof: Proof. unfold regex.lang. intro w. revert u H. induction w; intros u H. unfold derivs. now rewrite epsilon_eval by apply H. unfold derivs. setoid_rewrite <- IHw. clear IHw. revert w. apply lang_weq, deriv_eval; apply H. split. 2: apply H. apply is_01_mx_dot. apply H. apply is_01_mx_epsilon. Qed.
imports: positives comparisons kleene regex rmx sums matrix_ext prop normalisation