diff --git a/chap_5/e5_8.dfy b/chap_5/e5_8.dfy
index e69de29..748102c 100644
--- a/chap_5/e5_8.dfy
+++ b/chap_5/e5_8.dfy
@@ -0,0 +1,92 @@
+datatype Expr = Const(nat) | Var(string) | Node(op: Op, args: List<Expr>)
+
+datatype Op = Add | Mul
+
+datatype List<T> = Nil | Cons(head: T, tail: List<T>)
+
+function Eval(e: Expr, env: map<string, nat>): nat
+  requires GoodEnv(e, env)
+{
+  match e
+  case Const(c) => c
+  case Var(s) => env[s]
+  case Node(op, args) => EvalList(op, args, env)
+}
+
+/* E.4.9 => The default decreases clause use lexicographical ordering of the arguments.
+This implies the following decreases clause:
+    decreases op, args, env
+
+But as "op" is either Add or Mul which and does not have fixed order in a list<Expr>
+it jumps around.
+for example 10 * 5 + 3 * 10. 
+=> Node(Mul, Cons(Const(10), Cons()))
+
+*/
+
+function EvalList(args: List<Expr>, op: Op, 
+                  env: map<string, nat>): nat
+  decreases args
+  requires GoodEnvList(args, env)
+{
+  match args
+  case Nil =>
+    (match op case Add => 0 case Mul => 1)
+  case Cons(e, tail) =>
+    var v0, v1 := Eval(e, env), EvalList(tail, op, env);
+    match op
+    case Add => v0 + v1
+    case Mul => v0 * v1
+}
+
+predicate GoodEnv(e: Expr, env: map<string, nat>) {
+  match e
+  case Const(_) => true
+  case Var(s) => s in env.Keys
+  case Node(_, args) => GoodEnvList(args, env)
+}
+
+predicate GoodEnvList(args: List<Expr>, env: map<string, nat>)
+{
+  match args
+  case Nil => true
+  case Cons(e, tail) => GoodEnv(e, env) && GoodEnvList(tail, env)
+}
+
+function Substitute(e: Expr, n: string, c: nat): Expr
+{
+  match e
+  case Const(_) => e
+  case Var(s) => if s == n then Const(c) else e
+  case Node(op, args) => Node(op, SubstituteList(args, n,
+                                                 c))
+}
+function SubstituteList(es: List<Expr>, n: string, c: nat):
+  List<Expr>
+{
+  match es
+  case Nil => Nil
+  case Cons(e, tail) =>
+    Cons(Substitute(e, n, c), SubstituteList(tail, n, c))
+}
+
+lemma {:induction false} EvalSubstitute(e: Expr, n: string, c: nat, env: map<string, nat>)
+    ensures Eval(Substitute(e, n, c), env) == Eval(e, env[n:=c])
+{
+    match e
+    case Const(_) =>
+    case Var(_) =>
+    case Node(op, args) =>
+        EvalSubstituteList(args, op, n, c, env);
+}
+
+lemma {:induction false} EvalSubstituteList(
+    args: List<Expr>, op: Op, n: string, c: nat, env: map<string, nat>)
+    ensures EvalList(SubstituteList(args, n, c), op, env) == EvalList(args, op, env[n:= c])
+{
+    match args
+    case Nil =>
+    case Cons(e, tail) =>
+        EvalSubstitute(e, n, c, env);
+        EvalSubstituteList(tail, op, n, c, env);
+}
\ No newline at end of file