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