Unfolding a semireducible definition outside of tactics

Stream: general

[Vilim Lendvaj]

I want to build a certain structure, where the type of one field is dependent on the value of another.
If I set the value of the dependee to a semireducible definition, then the name of that definition shows up in the inferred type of the dependent.
Is it possible to unfold that definition so that the type of the dependent uses its right-hand side instead?
I know I can unfold definitions using tactics, but is there a simple way to do it directly in functional code?

[Kenny Lau]

Do you have an example? (#mwe)