checker2: inference rules; add beta reduction