proposition: Lemma star_nil_rw: Nil * == Nil.
proof: Proof. split; intros. - apply star_to_pow in H. destruct H as (n, H). apply nil_pow_in_inv in H. subst. apply nil_in. - apply nil_in_inv in H. subst. apply star_in_nil. Qed.
imports: Coq.Lists.List