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