Error while proving `Some(x, op)' = Some(x', op')` when `op` is an operator.

[kape1395]

I noticed a strange behavior while trying to prove something like Some(x, op)' = Some(x', op') where op is an operator.
My initial attempt was similar to THEOREM Fails1.
In my case, I resolved it by taking the approach like in THEOREM Works2 (wrapping the operator into a lambda).
I'm not sure if that's a bug, but I'm reporting it here just in case.

---- MODULE BugLambdaPrimed ----

Some(S, op(_)) == \A x \in S : op(x)

THEOREM Works1 ==
    ASSUME NEW x, NEW op(_)
    PROVE Some(x, op)' = Some(x', op') \* Invalid number of arguments if Fails1 is added.
    OBVIOUS

THEOREM Fails1 ==
    ASSUME NEW x, NEW op(_)
    PROVE Some(x, op)' = Some(x', op')
    BY DEF Some

THEOREM Works2 ==
    ASSUME NEW x, NEW op(_)
    PROVE Some(x, op)' = Some(x', LAMBDA y : op(y)')
    BY DEF Some

====