val2(plus(X, Y), Context, Value) :-
t(1), let(y, const(2), var(y))), nil, X) val2(X, Context, XValue),
  val2(Y, Context, YValue),
  Value is XValue + YValue.
val2(times(X, Y), Context, Value) :-
  val2(X, Context, XValue),
  val2(Y, Context, YValue),
  Value is XValue * YValue.
val2(const(X), _, X).
val2(var(X), Context, Value) :-
  lookup(X, Context, Value).
val2(let(X, Exp1, Exp2), Context, Value2) :-
  val2(Exp1, Context, Value1),
  val2(Exp2, [bind(X, Value1) | Context], Value2).

lookup(Variable, [bind(Variable, Value)|_], Value).
lookup(VarX, [bind(VarY, _)|Rest], Value) :-
  VarX \= VarY, lookup(VarX, Rest, Value).

/*
   val2(let(y, const(1), let(y, const(2), var(y))), nil, X).
 
   val2(let(a, plus(const(3), const(4)), times(var(a), const(5))), nil, V).
 */