proposition: Lemma union_comm_assoc : forall E F G, E \u (F \u G) = F \u (E \u G).
proof: Proof. Proof using. intros. rewrite union_assoc. rewrite (union_comm E F). rewrite~ <- union_assoc. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)