test030a.idr:12:26-14:1: When checking right hand side of testReflect1: When checking an application of function Reflect.getJust: Type mismatch between IsJust (Just x1) (Type of ItIsJust) and IsJust (prove (getProof x)) (Expected type) Specifically: Type mismatch between Just x and Nothing