expected

test030a.idr:12:14:When elaborating right hand side of testReflect1:
Can't unify
        IsJust (Just x)
with
        IsJust (prove (getProof x))

Specifically:
        Can't unify
                Just x
        with
                Nothing