proposition: Lemma cheminA_monoid : forall (w : Word) (q qd qaA dA : Ensf), automate_A q qd qaA dA -> forall e1 e2 : Elt, chemin_A q dA e1 e2 w -> inmonoid alph w.
proof: Proof. intros. elim H0; auto. Qed.
imports: Ensf Max Words Dec