proposition: Lemma equiv_l_egal_eqwordset : forall a b : wordset, l_egal a b <-> eqwordset a b.
proof: Proof. intros a b. unfold iff in |- *. split. intro Hyp; elim Hyp; auto. intros Hyp. split; unfold l_inclus in |- *; intro w; elim (Hyp w); auto. Qed.
imports: Ensf Words