[finite-model-theory] LUW July 6: Unification in Pretabular Extensions of S4