expected

Reflect.idr:173:21-26:
This style of tactic proof is deprecated. See %runElab for the replacement.
Reflect.idr:182:21-26:
This style of tactic proof is deprecated. See %runElab for the replacement.
Reflect.idr:190:15-20:
This style of tactic proof is deprecated. See %runElab for the replacement.
test030a.idr:12:26-14:1:
When checking right hand side of testReflect1 with expected type
        ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs

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