Two sequences are bigly equal iff the kernel of their difference is in φ
Ultraproduct, but on a general filter
Equivalence class containing the constant sequence of a term in β
Lift function to filter product
Lift binary operation to filter product
Lift properties to filter product
Lift binary relations to filter product