[sn9]

You can just type in `rfl` to assert that `37 = 37` (or anything of the form `X = X`).

[hammock]

I typed in rfl and hit execute and nothing happened (it added a line above but did not say I solved anything)