proposition: Lemma chemin_lettre : forall (e1 e2 x : Elt) (q d : Ensf), dans x alph -> dans e1 q -> dans e2 q -> dans (couple e1 (couple x e2)) d -> chemin e1 e2 q d (cons x nil).
proof: Proof. intros. apply chemin_cons with e2; auto. Qed.
imports: Ensf Max Words Dec