reg044.idr:4:6-11:
This style of tactic proof is deprecated. See %runElab for the replacement.
reg044.idr:4:4:When checking right hand side of Main.pf:
Type mismatch between
        b = b (Type of Refl)
and
        a = b (Expected type)

Specifically:
        Type mismatch between
                b
        and
                a