Keyword: unfold

To "unfold" a definition is to substitute its right-hand side (body) for its left-hand side (head).

Most definitions are unfolded automatically. An explicit or recursive definition must be unfolded manually using the unfold tactic.