ClaimAndUnfocus.idr:8:27-31:
  |
8 | ClaimAndUnfocus.foo_rhs = proof
  |                           ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.