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).