proposition: Lemma Recislang : forall q qd qa d : Ensf, automate q qd qa d -> islanguage alph (reconnait q qd qa d).
proof: Proof. intros. unfold islanguage at 1 in |- *. intro. unfold reconnait at 1 in |- *. intro. elim H0. intros. assumption. Qed.
imports: Ensf Max Words Dec