proposition: Lemma union_assoc : forall E F G, E \u (F \u G) = (E \u F) \u G.
proof: Proof. Proof using. intros. apply fset_extens; intros x; rewrite_all* in_union. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)