proposition: Lemma lang_deriv_dot_1 a (H K: lang'): H nil -> lang_deriv a (H⋅K) ≡ lang_deriv a H ⋅ K + lang_deriv a K.
proof: Proof. intros Hnil w; simpl; unfold lang_deriv, lang_dot. split. intros [[|b u] Hu [v Kv E]]; simpl in E. right. now rewrite E. injection E; intros -> <-; clear E. left. repeat eexists; eauto. intros [[u Hu [v Kv ->]]|Ka]; repeat eexists; eauto. Qed.
imports: List prop monoid