proposition: Lemma star_void_rw: {} * == Nil.
proof: Proof. split; intros. - destruct H as (n, H). apply void_pow_in_inv in H. subst. apply nil_in. - apply nil_in_inv in H. subst. exists 0. apply pow_nil. Qed.
imports: Coq.Lists.List