# Unfolding expressions in Coq by one layer

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.

• If it's does what you want I'd say it's good enough. You could define your own ltac tactic so as not to write the match goal every time. May 14 at 20:25
• coq.inria.fr/refman/proofs/writing-proofs/… May 14 at 22:15