proposition: Lemma automate_def1 : forall q qd qa d : Ensf, automate q qd qa d -> inclus d (prodcart q (prodcart alph q)).
proof: Proof. intros q qd qa d H. elim H. intros H1 H0; elim H0; clear H0. auto. Qed.
imports: Ensf Max Words Dec