proposition: Lemma lwordnil_is_reg : isregular (lword nil).
proof: Proof. cut (exists q : Ensf, (exists e : Elt, (exists qa : Ensf, (exists d : Ensf, automate q (singleton e) qa d /\ eqwordset (reconnait q (singleton e) qa d) (lword nil))))). 2: apply lwordnil_is_regS; auto. intro H; elim H; clear H. intros q H; elim H; clear H. intros e H; elim H; clear H. intros qa H; elim H; clear H. intros d H; elim H; clear H. intros. red in |- *. exists q. exists (singleton e). exists qa. exists d. auto. Qed.
imports: Ensf Max Words Dec Reg Rat