---

Step * 1 of Lemma callbyvalueall-apply2


1. g : Base
2. a : Top
3. F : Top
4. g ~ λx.(g x)
⊢ let f ⟵ g
  in let x ⟵ f a
     in F[x] ~ let x ⟵ g a
               in F[x]
BY
{ (BLemma `callbyvalueall-apply` THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  Base
2.  a  :  Top
3.  F  :  Top
4.  g  \msim{}  \mlambda{}x.(g  x)
\mvdash{}  let  f  \mleftarrow{}{}  g
    in  let  x  \mleftarrow{}{}  f  a
          in  F[x]  \msim{}  let  x  \mleftarrow{}{}  g  a
                              in  F[x]


By

---

Latex:
(BLemma  `callbyvalueall-apply`  THEN  Auto)

---

Home Index