proposition: Lemma star_star_rw: forall (L:language), L * * == L *.
proof: Proof. intros. split; intros. - apply star_to_pow in H. destruct H as (n, Hn). generalize dependent w. induction n; intros. { inversion Hn; subst; clear Hn. apply star_in_nil. } inversion Hn; subst; clear Hn. apply IHn in H0. apply app_star_rw. auto using app_in_eq. - destruct H as (n, H). exists 1. apply pow_cons with (w1:=w) (w2:=nil). + apply pow_nil. + exists n. assumption. + auto with *. Qed.
imports: Coq.Lists.List