feat(logic/embedding): use simps (#4169)
Some lemmas are slightly reformulated, and have a worse name. But they are (almost) never typed explicitly, since they are simp lemmas (even the occurrences in other files probably came from `squeeze_simp`).
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
