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: Jan 17 2026 at 20:25 UTC