exp : type.

abs : (exp -> exp) -> exp.


app : exp -> exp -> exp.

step : exp -> exp -> type.