Add a notion of type equality in the client

We can now introduce and use type equalities using a Refl/Use construct in System F.