fact: Definition Chemin (e1 e2 : Elt) (q d : Ensf) (w : Word) : Prop := match w return Prop with | nil => dans e1 q /\ e1 = e2 :>Elt | cons a w' => exists e : Elt, chemin e e2 q d w' /\ dans e1 q /\ dans a alph /\ dans (couple e1 (couple a e)) d end.
imports: Ensf Max Words Dec