for the few of us.

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on R∘, it is monotonic on lax preorder ∋ . R. Furthermore, prune (∋ . R) = thin R. Therefore, pruning is a generalisation of thinning. We need the notion of lax preorders because, for some problems, the generating relation S is monotonic on a lax preorder, but not a preorder.

Prove the thinning theorem by fold fusion. Horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years?