tp : type.
arrow : tp -> tp -> tp.
unit : tp.

tm : type.
empty : tm.
app : tm -> tm -> tm.
lam : tp -> (tm -> tm) -> tm.

of : tm -> tp -> type.
of-empty : of empty unit.
of-lam : of (lam T2 ([x] E x)) (arrow T2 T)
          <- ({x: tm} of x T2 -> of (E x) T).
of-app : of (app E1 E2) T
          <- of E1 (arrow T2 T)
          <- of E2 T2.

value : tm -> type.
value-empty : value empty.
value-lam : value (lam T ([x] E x)).

step : tm -> tm -> type.
step-app-1 : step (app E1 E2) (app E1' E2)
              <- step E1 E1'.
step-app-2 : step (app E1 E2) (app E1 E2') 
              <- value E1
              <- step E2 E2'.
step-app-beta : step (app (lam T2 ([x] E x)) E2) (E E2)
                 <- value E2.