proposition: Lemma chemin_A_d1_d2 : forall (q d1 d2 : Ensf) (w : Word) (e1 e2 : Elt), chemin_A q d1 e1 e2 w -> inclus d1 d2 -> chemin_A q d2 e1 e2 w.
proof: Proof. intros q d d2 w e1 e2 H. elim H; clear H. auto. intros. apply chemin_A_cons with e; auto. intros. apply chemin_A_epsilon with e; auto. Qed.
imports: Ensf Max Words Dec