solve constraints with inert right-hand sides

Given a constraint
  _X us == D vs
where D is an inert definition (data/record/var/con) we can solve
  _X := \ xs -> D (_Ys xs)
provided that
  - us are all neutral, to ensure that _X cannot reduce to D
  - none of us have D as head
This is important for instance search where knowing the head D can
enable progress.
updated instance argument examples for recursive search
don't treat constructors as inert

not needed for instance search and it can lead to unsolved metas
(see test/succeed/InertFailure.agda)
fixed bugs in inert improvement
moved documentation from CHANGELOG to release-notes/2-4-2