Revert to old approach definitions

[jellooo038]

• Just use built-in definitions system, so explicit mentioning the use of definitions is not mandatory (or possible).
• Reworked 'Expand the definition of ...' tactic:
  • it now throws errors suggesting to use a different tactic with a similar effect as unfolding the definitions instead of wrapping the proof goal;
  • it now expects as input a statement in which to expand the definitions instead of a clause indicating whether to expand in the proof goal or a hypothesis.