exp : type.

z    : exp.
s    : exp -> exp.
case' : exp -> exp -> (exp -> exp) -> exp.
pair : exp -> exp -> exp.
fst  : exp -> exp.
snd  : exp -> exp.
lam  : (exp -> exp) -> exp.
app  : exp -> exp -> exp.
letv : exp -> (exp -> exp) -> exp.
letn : exp -> (exp -> exp) -> exp.
fix  : (exp -> exp) -> exp.


eval : exp -> exp -> type.
ev_z : eval z z.
ev_s : eval E V -> eval (s E) (s V).
ev_case'_z :
      eval E1 z -> eval E2 V -> eval (case' E1 E2 (\x. E3 x)) V.

ev_case'_s :
      eval E1 (s V1') -> eval (E3 V1') V -> eval (case' E1 E2 (\x. E3 x)) V.

ev_pair :
      eval E1 V1 -> eval E2 V2 -> eval (pair E1 E2) (pair V1 V2).

ev_fst : eval E (pair V1 V2) -> eval (fst E) V1.
ev_snd : eval E (pair V1 V2) -> eval (snd E) V2.
ev_lam : eval (lam (\x. E x)) (lam (\x. E x)).


ev_app :
      eval E1 (lam (\x. E1' x)) -> eval E2 V2 -> eval (E1' V2) V -> eval (app E1 E2) V.

ev_letv :
      eval E1 V1 -> eval (E2 V1) V -> eval (letv E1 (\x. E2 x)) V.

ev_letn :
      eval (E2 E1) V -> eval (letn E1 (\x. E2 x)) V.

ev_fix : eval (E (fix (\x. E x))) V -> eval (fix (\x. E x)) V.
