proposition: Lemma I_i : forall (X : Ensf) (w : Word), Inmonoid X w -> inmonoid X w.
proof: Proof. intros X. simple induction w. auto. intros x w0 H H0. cut (dans x X /\ Inmonoid X w0); auto. intro H1; elim H1; clear H1. auto. Qed.
imports: Ensf