feat: abbrev produces theorems where appropriate

feat: abbrev produces theorems where appropriate #24980