pub open spec fn associative<T>(r: FnSpec<(T, T), T>) -> bool
{ forall |x: T, y: T, z: T| #[trigger] r(x, r(y, z)) == #[trigger] r(r(x, y), z) }