lcnfCache.lean:16:4-16:18: warning: declaration uses `sorry`