Improve usage of locally-defined lambdas

[iamrecursion]

It is not an uncommon pattern to locally define a lambda and then pass it to a function that will use it. Unfortunately, the current state of steps will smoosh the entire Expr that defines the lambda into the precondition of the goal, which makes it a pain to provide semantics for.

This can currently be worked around using:

  apply STHoare.consequence_frame
  with_unfolding_all apply sort_via_spec
  case h_ent => sl
  case q_ent => intros; sl; assumption
  any_goals assumption

In future, it would be nice to introduce a tactic generalize_binding name newName which looks for a binding in the precondition of the form name ↦ expr. It would alter the proof state such that the precondition has name ↦ newName and a local binding let newName := expr. This would make it possible to locally state and prove semantics for the bound expression.