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 with expected type
        (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

Type mismatch between
        b = b (Type of Refl)
and
        a = b (Expected type)

Specifically:
        Type mismatch between
                b
        and
                a