proposition: Lemma chemin_chemin_A : forall (q d : Ensf) (w : Word) (e1 e2 : Elt), chemin e1 e2 q d w -> chemin_A q d e1 e2 w.
proof: Proof. intros q d w e1 e2 H. elim H; clear H. auto. intros. apply chemin_A_cons with e0; auto. Qed.
imports: Ensf Max Words Dec