proposition: Lemma deriv_traces a i e: lang (deriv a i e) ≡ traces_deriv a i (lang e).
proof: Proof. symmetry. induction e; simpl deriv. simpl lang. rewrite lang_ofbool. apply traces_deriv_single. rewrite lang_0. apply traces_deriv_inj. setoid_rewrite traces_deriv_pls. now apply cup_weq. generalize (epsilon_iff_lang_nil a e1). case epsilon; intro He1. fold_ugregex. setoid_rewrite dot1x. simpl lang. setoid_rewrite traces_deriv_dot_1. now rewrite IHe1, IHe2. now rewrite <-He1. fold_ugregex. setoid_rewrite dot0x. rewrite cupxb. simpl lang. setoid_rewrite traces_deriv_dot_2. now rewrite IHe1. rewrite <-He1. discriminate. simpl lang. setoid_rewrite traces_deriv_itr. now rewrite IHe, str_itr, <-inj_top. Qed.
imports: kat lsyntax positives sups glang comparisons boolean