proposition: Lemma app_star_rw: forall (L:language), L * >> L * == L * .
proof: Proof. split; intros. - apply app_in_inv in H. destruct H as (w1, (w2, (?, (Ha, Hb)))). subst. destruct Ha as (n1, Ha). destruct Hb as (n2, Hb). exists (n1 + n2). apply pow_add; auto. - apply app_in_eq with (w1:=[]) (w2:=w). + apply star_in_nil. + assumption. Qed.
imports: Coq.Lists.List