proposition: Lemma chemin_Chemin : forall (e1 e2 : Elt) (q d : Ensf) (w : Word), chemin e1 e2 q d w -> Chemin e1 e2 q d w.
proof: Proof. intros e1 e2 q d w H; elim H; clear H. intros. red in |- *; simpl in |- *; auto. intros. red in |- *; simpl in |- *. exists e0. auto. Qed.
imports: Ensf Max Words Dec