proposition: Lemma star_any_rw: Any * == All.
proof: Proof. split; intros. - apply all_in. - unfold Star. generalize dependent H. induction w; intros. { exists 0. apply pow_nil. } assert (All w) by auto using all_in. destruct IHw as (n, Hp); auto. exists (S n). rewrite in_def in *. apply pow_cons with (w1:=[a]) (w2:=w); auto. rewrite in_def. auto using any_in. Qed.
imports: Coq.Lists.List