[Agda] unfolding just a single definition in the context of a goal

[Marcus Christian Lehmann]

Dear Agda community,

When in in context of a goal, Is there a way to have just one definition 
unfolded instead of a complete normalization that is performed on `C-u 
C-u C-c C-,` ?

For example: in the notes of M. Escardó [1] there is something like

   sets-have-wconstant-≡-endomaps' : (X : Type ℓ) → is-set X → 
wconstant-≡-endomaps X
   sets-have-wconstant-≡-endomaps' X p = {!!}

Now, in the hole {!!}, whe using `C-c C-,` or `C-u C-c C-,`this gives a

   Goal: wconstant-≡-endomaps X
————————————————————————————————————————————————————————————
   p : is-set X
   X : Type ℓ

where `C-u C-u C-c C-,` normalizes all terms and gives

   Goal: (x y : X) →
         Σ (λ f → (x₁ x' : Id X x y) → Id (Id X x y) (f x₁) (f x'))
————————————————————————————————————————————————————————————
   p : (x y : X) (x₁ y₁ : Id X x y) → Id (Id X x y) x₁ y₁
   X : Set ℓ

In this case my question is whether it is possible to have just one 
definition unfolded, e.g. just have `is-set` unfolded and get an 
intermediate result like

   Goal: wconstant-≡-endomaps X
————————————————————————————————————————————————————————————
   p : (x y : X) → is-subsingleton (x ≡ y)
   X : Type ℓ

I could not find any hints about that in the agda documentation.

kind regards,
Christian

[1] 
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#setscharacterization