proposition: Lemma eqwordset_trans : forall l1 l2 l3 : wordset, eqwordset l1 l2 -> eqwordset l2 l3 -> eqwordset l1 l3.
proof: Proof. unfold eqwordset in |- *. intros. elim (H0 w); clear H0; intros. elim (H w); clear H; intros. auto. Qed.
imports: Ensf