module cbv.
import forumlog.

kind tm     type.
type abs    (tm -> tm) -> tm.
type app    tm -> tm -> tm.

type eval   tm -> tm -> o -> o.

cl (eval (abs M) (abs M) K o- K).
cl (eval (app M N) V K o- eval M (abs R) (eval N U (eval (R U) V K))).