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