Reflect.idr:207:38:When elaborating right hand side of testReflect1: When elaborating an application of function Reflect.getJust: Can't unify IsJust (Just x) with IsJust (prove (getProof x)) Specifically: Can't unify Just x with Nothing