proposition: Lemma inmonoid_cons_inv : forall (X : Ensf) (w : Word) (a : Elt), inmonoid X (cons a w) -> inmonoid X w.
proof: Proof. intros. cut (Inmonoid X w); auto. cut (Inmonoid X (cons a w)); auto. intro H0. cut (dans a X /\ Inmonoid X w); auto. intro H1; elim H1; clear H1. auto. Qed.
imports: Ensf