proposition: Lemma induction_star : forall (P : Word -> Prop) (l : wordset), (forall (n : nat) (w : Word), lpuiss n l w -> P w) -> forall w : Word, lstar l w -> P w.
proof: Proof. unfold lstar in |- *. intros. elim H0; clear H0. intros x H0. apply (H x w); auto. Qed.
imports: Ensf Words