Yes, it does, and what you said makes sense.

Really, the intent of the invariant isn’t “zonkedness” per se, but merely that the type of the evidence should be “at least as zonked” as ctev_pred is. But that is a little vague and handwavy, so I’ll go the route you suggest and just reword things a little to explain.

Thanks!