proposition: Lemma lwordnil_is_regS : 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)))).
proof: Proof. exists (singleton zero). exists zero. exists (singleton zero). exists (prodcart empty (prodcart alph empty)). split. red in |- *; auto. red in |- *; split. red in |- *. symmetry in |- *; apply lwordnil_is_reg2. assumption. intro. compute in H. rewrite <- H. apply lwordnil_is_reg1. Qed.
imports: Ensf Max Words Dec Reg Rat