---

Step * of Lemma callbyvalue-then-apply

∀[f,x:Top].  (eval g = f in g x ~ f x)
BY
{ (Auto
   THEN SqEqualTopToBase
   THEN SqequalSqle
   THEN AssumeHasValue
   THEN Try (((HasValueD (-1) THEN Auto) THEN CallByValueReduce 0 THEN Auto))
   THEN ExceptionCases (-1)
   THEN Try ((CallByValueReduce 0 THEN Complete (Auto)))
   THEN ExceptionSqequal (-1)
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,x:Top].    (eval  g  =  f  in  g  x  \msim{}  f  x)


By

---

Latex:
(Auto
  THEN  SqEqualTopToBase
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  Try  (((HasValueD  (-1)  THEN  Auto)  THEN  CallByValueReduce  0  THEN  Auto))
  THEN  ExceptionCases  (-1)
  THEN  Try  ((CallByValueReduce  0  THEN  Complete  (Auto)))
  THEN  ExceptionSqequal  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index