Commit 2020-06-23 13:58 d287d345

refactor(order/filter/basic): define filter.eventually_eq (#3134)

• Define eventually_eq (f =^f[l] g) and eventually_le (f ≤^f[l] g).
• Use new notation and definitions in some files.