proposition: Lemma epsilon_deriv_pure_mx a n m (M: rmx n m): is_pure_mx M -> epsilon_mx (deriv_mx a M) ≡ deriv_mx a M.
proof: Proof. intros H i j. apply epsilon_deriv_pure, H. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation