logical relation
n : a relation between propositions
logical relation
A {relation} R satisfying
f R g <=> For all a, b, a R b => f a R g b
This definition, by Plotkin, can be used to extend the
definition of a relation on the types of a and b to a relation
on functions.