Are there any ways to unfold an expression in Coq by a single layer?
I have only come up with this obvious solution:
Parameter X : Set.
Definition Y := X.
Definition Z := Y.
Goal Z.
match goal with
| |- ?h => unfold h
end.
(*
================
Y
*)
Abort.
But for sure there are better and more elegant ways to do it.
match goal
every time. $\endgroup$