XE : xeval (app (lam [x] (vl x)) z) V.

XE : xeval (app (fix [double] lam [x]
		  case (vl x) z
		  [x'] s (s (app double (vl x')))) (s (s (s z))))
     V.