exp : type.
z : exp.
s : exp -> exp.
case : exp -> exp -> (exp -> exp) -> exp.
lam : (exp -> exp) -> exp.
app : 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 ([y:exp] E3 y)) V.
ev_case_s : eval (case E1 E2 E3) V
         <- eval E1 (s V1)
         <- eval (E3 V1) V.
ev_lam : eval (lam F) (lam F).
ev_app : eval (app E1 E2) V
         <- eval E1 (lam F) 
         <- eval E2 V2 
         <- eval (F V2) V.
ev_fix : eval (E1 (fix E1)) V -> eval (fix E1) V.
double : exp = 
  fix ([double : exp] 
    (lam [i : exp] 
      (case i z ([iminusone : exp] (s (s (app double iminusone))))))).
%mode eval +A -B.

 %query 1 1 eval (app double (app double (app double (s (s (s z)))))) V.