I got as far as, well, you've got t of type tau, and then you've got your lots-of-spaces operator, and you're applying it to a function on t which you don't seem to have declared (although I see you did declare a more complicated function to be a "proposition", and sure enough there it is in the denominator).

So... um, I guess a proposition returns a boolean, right? So you're dividing lots-of-spaces-operator(t-of-type-tau, undefined-function) by a boolean, and I feel like that's probably a type error.

This isn't going to stop me from commenting, mind. ^_^