Matthew - I thought Michael was taking a different approach than the one I suggested: proving that \$$\Phi(x',y') = \text{true}\$$ if \$$\Phi(x,y) = \text{true}\$$, \$$x' \le x\$$ and \$$y \le y'\$$. This uses the 'original' definition of enriched profunctor, which I expanded to a lengthier definition in the theorem in [Lecture 56](https://forum.azimuthproject.org/discussion/2280/lecture-56-chapter-4-feasibility-relations/p1).

Of course, if this is what Michael was doing, it counts as bad style not to mention it!

Basically, if a smart mathematician who knows the subject matter doesn't understand your proof, there's probably a way to improve the proof.