proposition: Lemma lw_imp_lstarlw : forall (l : wordset) (w : Word), l w -> lstar l w.
proof: Proof. intros. unfold lstar in |- *. exists 1. change (lconc l (lpuiss 0 l) w) in |- *. unfold lconc in |- *. exists w. exists nil. split; [ assumption | split ]. unfold lpuiss in |- *. unfold lword in |- *; auto. symmetry in |- *. apply Append_w_nil. Qed.
imports: Ensf Words