proposition: Lemma i_I : forall (X : Ensf) (w : Word), inmonoid X w -> Inmonoid X w.
proof: Proof. intros X w H. elim H. red in |- *; simpl in |- *; exact I. intros. change (dans e X /\ Inmonoid X w0) in |- *. auto. Qed.
imports: Ensf