proposition: Lemma inter_comm_assoc : forall E F G, E \n (F \n G) = F \n (E \n G).
proof: Proof. Proof using. intros. rewrite inter_assoc. rewrite (inter_comm E F). rewrite~ <- inter_assoc. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)