Library Waterproof.Notations.IndexedSets
Require Import Libs.Sets.IndexedOperations.
Require Import Notations.Sets.
Notation "⋂_{ i Q } X_i" := (indexed_intersection Q%pfs (fun i => X_i)) (at level 30, i binder) : subset_scope.
Notation "⋃_{ i Q } X_i" := (indexed_union Q%pfs (fun i => X_i)) (at level 30, i binder).
Require Import Notations.Sets.
Notation "⋂_{ i Q } X_i" := (indexed_intersection Q%pfs (fun i => X_i)) (at level 30, i binder) : subset_scope.
Notation "⋃_{ i Q } X_i" := (indexed_union Q%pfs (fun i => X_i)) (at level 30, i binder).