test029.idr:29:25-30: This style of tactic proof is deprecated. See %runElab for the replacement. test029.idr:36:25-30: This style of tactic proof is deprecated. See %runElab for the replacement.