proposition: Lemma sync_d_def : forall (e1 e2 x : Elt) (q dA : Ensf), dans x alph -> chemin_A q dA e1 e2 (cons x nil) -> dans (couple e1 (couple x e2)) (sync_d q dA).
proof: Proof. intros. unfold sync_d in |- *. apply imp_dans_tq; auto. apply coupl2_inv. apply (dansA_e1_q q dA (cons x nil) e1 e2); auto. apply coupl2_inv; auto. apply (dansA_e2_q q dA (cons x nil) e1 e2); auto. Qed.
imports: Ensf Max Words Dec