proposition: Lemma chemin_A_q1_q2 : forall (q1 q2 d : Ensf) (e1 e2 : Elt) (w : Word), chemin_A q1 d e1 e2 w -> inclus q1 q2 -> chemin_A q2 d e1 e2 w.
proof: Proof. intros q1 q2 d 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