proposition: Lemma sync_d_def2 : forall (e1 e2 x : Elt) (q dA : Ensf), dans x alph -> dans (couple e1 (couple x e2)) (sync_d q dA) -> chemin_A q dA e1 e2 (cons x nil).
proof: Proof. intros e1 e2 x q dA H. unfold sync_d in |- *. intro. cut (dans (couple e1 (couple x e2)) (prodcart q (prodcart alph q)) /\ est_dans_d q dA (couple e1 (couple x e2))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht. intro H1. unfold est_dans_d in |- *. unfold est_dans_d2 in |- *. auto. Qed.
imports: Ensf Max Words Dec