proposition: Lemma inmonoid_map : forall (f : Elt -> Elt) (a : Ensf) (w : Word), inmonoid a w -> inmonoid (map f a) (Word_ext f w).
proof: Proof. intros. elim H; [ unfold Word_ext in |- *; auto | idtac ]. intros; unfold Word_ext in |- *; simpl in |- *. apply inmonoid_cons; try apply dans_map_inv; auto. Qed.
imports: Ensf