2634.lean:5:2-5:31: error: `simp` made no progress
hello