Hi! I'm observing clarsimp spinning indefinitely in one proof step (simp is fine) and wonder how I could debug what's going on. Any suggestions?
clarsimp
simp
Last updated: Apr 14 2026 at 09:21 UTC