proposition: Lemma trans_dA_d : forall (q dA : Ensf) (e0 e x : Elt), dans e0 q -> dans x alph -> dans e q -> dans (couple e0 (couple x e)) dA -> dans (couple e0 (couple x e)) (sync_d q dA).
proof: Proof. intros. cut (chemin_A q dA e0 e (cons x nil)). intro. unfold sync_d in |- *. apply imp_dans_tq; auto. cut (chemin_A q dA e e nil); auto. intro. apply chemin_A_cons with e; auto. Qed.
imports: Ensf Max Words Dec