Reflect.idr:175:21-25:
    |
175 | Reflect.appRExpr1 = proof {
    |                     ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

Reflect.idr:184:21-25:
    |
184 | Reflect.appRExpr2 = proof {
    |                     ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

Reflect.idr:192:15-19:
    |
192 | Reflect.bp1 = proof {
    |               ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

test030a.idr:12:26-37:
   |
12 | testReflect1 {a} xs ys = AssocProof a
   |                          ~~~~~~~~~~~~
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 (snd x)) (Expected type)
        
        Specifically:
                Type mismatch between
                        Just x
                and
                        Nothing