proposition: Lemma extension_qd : forall (w : Word) (e0 e1 e2 e3 a : Elt) (q d : Ensf), chemin e1 e2 q d w -> chemin e1 e2 (add e0 q) (add (couple e0 (couple a e3)) d) w.
proof: Proof. simple induction w. intros. cut (Chemin e1 e2 q d nil); auto. intro. cut (dans e1 q /\ e1 = e2 :>Elt); auto. intro H1; elim H1; auto. intros x w0 H e0 e1 e2 e3 a q d H0. cut (Chemin e1 e2 q d (cons x w0)); auto. intro. cut (exists e : Elt, chemin e e2 q d w0 /\ dans e1 q /\ dans x alph /\ dans (couple e1 (couple x e)) d); auto. intro H2; elim H2; clear H2. intros e H2; elim H2; clear H2. intros H2 H3; elim H3; clear H3. intros H3 H4; elim H4; clear H4. intros H4 H5. apply (chemin_cons e e2 (add e0 q) (add (couple e0 (couple a e3)) d) w0 e1 x); auto. Qed.
imports: Ensf Max Words Dec Reg Rat