proposition: Lemma M_sum: M ≡ \sum_(a\in vars) M_(a).
proof: Proof. intros i j. simpl. rewrite (@expand' (M i j) (mx_vars M ++vars')). 2: apply leq_xcup; left; apply mx_vars_full. rewrite epsilon_pure by apply Hnfa. setoid_rewrite cupbx. setoid_rewrite mx_sup. apply sup_weq. 2: reflexivity. intro a. now rewrite <-epsilon_deriv_pure by apply Hnfa. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation