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