Is there an ssreflect equivalent of revert
(move: x
doesn't make it) here :
Goal let x := 1 in x * x = 1.
move=> x; revert x.
move: @x
?
I remember having seen a syntax for that (I assume you want to keep the def. of x
here)
thanks! didn't know it exists
Last updated: Oct 13 2024 at 01:02 UTC