val tc = "  app(abs(emptyEnv:->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))).              app(         abs(extendEnv:->(->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))),->(Char,->(mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))),->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))))).              app(app(fix(abs(f:->(->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))),->(mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )),mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))).abs(env:->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))).abs(tm:mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )).case tm of     Tru=v => tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))   | Fls=v => tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))   | Zero=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))   | Var=v => app(env, v)   | Abs=v => ( case app(app(f,                             app(app(app(extendEnv, env),project(v.var)),project(v.tp))                         ), project(v.t)) of                   Boolean=vv => tag (Arrow=record(fun=project(v.tp),                                                   arg=tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                 | Nat=vv => tag (Arrow=record(fun=project(v.tp),                                                   arg=tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                 | Arrow=vv => tag (Arrow=record(fun=project(v.tp),                                                   arg=tag(Arrow=vv as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))) as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                 | None=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                esac              )   | App=v => ( case app(app(f,env), project(v.fun)) of                     Arrow=vv => if =(project(vv.fun),                                      app(app(f,env), project(v.arg)))                                 then project(vv.arg)                                 else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                                 fi                   | Boolean=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                   | Nat=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                   | None=vv => tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                esac )   | If=v => if =(app(app(f,env),project(v.cond)), tag(Boolean=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))))             then ( if =(app(app(f,env),project(v.thn)), app(f,project(v.els)))                    then app(app(f,env),project(v.thn))                    else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                    fi )             else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))             fi   | Succ=v => if =(app(app(f,env),v), tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))))               then tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))               else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))               fi   | Pred=v => if =(app(app(f,env),v), tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))))               then tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))               else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))               fi   | Fix=v => ( case v of                    Abs=v => if =(app(app(f,env), project(v.t)), project(v.tp))                             then project(v.tp)                             else tag(None=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                             fi                  | Tru=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | Fls=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | Abs=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | App=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | If=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | Succ=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | Pred=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                  | Fix=v => tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))))                esac )   esac    )))),     emptyEnv),          tag(App=record(fun=tag(Abs=record(var='a',                                 tp=tag(Nat=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))),                                  t=tag(Var='a' as mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )))                             ) as mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit ))),                         arg=tag(Zero=# as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))))             as mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))) )          ),          abs(oldEnv:->(Char,mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x)))).             abs(s:Char.                 abs(n:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))).                     abs(sprime:Char.                         if =(s,sprime) then n else app(oldEnv,sprime) fi                     )                 )             )         )     )       ),     abs(s:Char.tag(none = # as mu(y.Variant(Tru:Unit, Fls:Unit, Zero:Unit, Var:Char, Abs:Record(var:Char, tp:mu(x.Variant(None:Unit, Boolean:Unit, Nat:Unit, Arrow:Record(in:x, out:x))), t:y), App:Record(fun:y, arg:y), If:Record(cond:y, thn:y, els:y), Succ:y, Pred:y, IsZero:y, Fix: y, None:Unit )))) )  "

val tcm = ps tc