- Twiggle with the burden of proof in log_related_arrow
- rel_rec_l/r returns a goal with an (unsimplified) lamsubst
  and can detect locked lambdas
- Fix some notational issues [hax.v]
- Rewrite the counter refinement proof to make greater use of lamsubst