ClaimAndUnfocus.idr:8:27-32:
This style of tactic proof is deprecated. See %runElab for the replacement.