proposition: Lemma extension_aut : forall (w : Word) (e0 e a : Elt) (q qa d : Ensf), reconnait q (singleton e) qa d w -> ~ dans e0 q -> dans a alph -> reconnait (add e0 q) (singleton e0) qa (add (couple e0 (couple a e)) d) (cons a w).
proof: Proof. unfold reconnait in |- *. intros. elim H; clear H. intros H H2; elim H2; clear H2. intros e12 H2; elim H2; clear H2. intros e2 H2; elim H2; clear H2. intros H2 H3. split; auto. exists e0. exists e2. split; auto. elim H3; clear H3; intros H3 H4. split; auto. cut (e12 = e :>Elt); auto. intro H5; rewrite <- H5. apply (chemin_cons e12 e2 (add e0 q) (add (couple e0 (couple a e12)) d) w e0 a); auto. apply extension_qd; auto. Qed.
imports: Ensf Max Words Dec Reg Rat