[Reduction Relation] where clause

[Beatriz Moreira]

Hello,

I was reading your documentation for the Reduction Relations (4.4), and we can use side-conditions and other extras like where and bind. But I cannot implement them in my code. Can someone show me an example of how do I use the clause where? For example, how do I verify that a variable f is the same f as the one in the pattern-sequence T f ( T x ).

Thank you!