proposition: Lemma star_union_nil_rw: forall L1, (Nil U L1) * == L1 *.
proof: Proof. intros. split; intros. - destruct H as (n, H). induction H. + apply star_in_nil. + subst. destruct H0. * inversion H0; subst; clear H0. simpl. assumption. * apply star_cons_eq; auto. - destruct H as (n, H). induction H. + apply star_in_nil. + subst. apply star_cons_eq; auto. right. assumption. Qed.
imports: Coq.Lists.List