proposition: Lemma Chemin_chemin : forall (e1 e2 : Elt) (q d : Ensf) (w : Word), Chemin e1 e2 q d w -> chemin e1 e2 q d w.
proof: Proof. intros e1 e2 q d. simple induction w. intro. cut (dans e1 q /\ e1 = e2 :>Elt); auto. intro H0; elim H0; clear H0. intros; apply chemin_nil; auto. intros x w0 H H0. 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 H1; elim H1. intros e H2; elim H2; clear H1 H2. intros H1 H2; elim H2; clear H2. intros H2 H3; elim H3; clear H3. intros. apply chemin_cons with e; auto. Qed.
imports: Ensf Max Words Dec