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