Is there an ssreflect equivalent of
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
thanks! didn't know it exists
Last updated: Feb 08 2023 at 07:02 UTC