reg017.idr:5:17-23:
  |
5 |       { default tactics { refine Refl; solve; } prfA : a = a } ->
  |                 ~~~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

reg017.idr:8:17-23:
  |
8 |       { default tactics { refine Refl; solve; } prfBC : b = c } ->
  |                 ~~~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

4