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