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.