Construct BI on monotone function spaces.

Title says it all. There's one admit left that I cannot figure out in line 267. Name suggestions from me are either "monfun" (as in the filename) or "funbi" (as in the contents). I actually prefer "monfun" now. I can do the renaming to whatever we end up with.

There's a comment about "uPred.emp" in there. I think I needed to unfold that to make everything work but I suppose we can solve that problem when it actually arises.