proposition: Lemma nouvx_dans_qa : forall (q qaA dA : Ensf) (e : Elt), dans e q -> (exists e' : Elt, dans e' qaA /\ chemin_A q dA e e' nil) -> dans e (sync_qa q qaA dA).
proof: Proof. intros. elim H0; clear H0. intros e' Ht; elim Ht; clear Ht. intros H0 H1. unfold sync_qa in |- *. apply union_d. apply imp_dans_tq; auto. exists e'; auto. Qed.
imports: Ensf Max Words Dec