proposition: Lemma deriv_01 a e: is_01 e -> deriv a e ≡ 0.
proof: Proof. induction 1; simpl deriv; fold_regex. reflexivity. reflexivity. rewrite IHis_01_1, IHis_01_2. apply cupI. rewrite IHis_01_1, IHis_01_2. ra. rewrite IHis_01. apply dot0x. Qed.
imports: syntax kleene boolean lang lset sums normalisation