proposition: Lemma chemin_Append : forall (e1 e e2 : Elt) (q d : Ensf) (w1 w2 : Word), chemin_A q d e1 e w1 -> chemin_A q d e e2 w2 -> chemin_A q d e1 e2 (Append w1 w2).
proof: Proof. intros e1 e e2 q d w1 w2 H. elim H. intros e0 e3 H0 H1 H2. simpl in |- *; rewrite H1; auto. intros. simpl in |- *. cut (chemin_A q d e3 e2 (Append w w2)); auto. intro. apply chemin_A_cons with e3; auto. intros. cut (chemin_A q d e3 e2 (Append w w2)); auto. intro. apply chemin_A_epsilon with e3; auto. Qed.
imports: Ensf Max Words Dec