proposition: Lemma lang_deriv_str a (H: lang'): lang_deriv a (H^*) ≡ lang_deriv a H ⋅ H^*.
proof: Proof. intro w. split. intros [n Hn]. induction n in a, w, Hn; simpl in Hn. discriminate. destruct Hn as [[|b v] Hv [u Hu Hw]]; simpl in Hw. rewrite <- Hw in Hu. apply IHn, Hu. injection Hw; intros -> ->; clear Hw. repeat eexists; eauto. intros [u Hu [v [n Hv] ->]]. exists (S n). repeat eexists; eauto. Qed.
imports: List prop monoid