---

Step * 1 of Lemma callbyvalueall-single-sqle2


1. F : Base
2. G : Base
3. a : Top
4. ∀b:Base. (G[[b]] ≤ F[b])
⊢ let x ⟵ [a]
  in G[x] ≤ let x ⟵ a
            in F[x]
BY
{ ((RWO "callbyvalueall-single" 0 THENA Auto) THEN SqLeTopToBase THEN UseCbvaSqle THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  F  :  Base
2.  G  :  Base
3.  a  :  Top
4.  \mforall{}b:Base.  (G[[b]]  \mleq{}  F[b])
\mvdash{}  let  x  \mleftarrow{}{}  [a]
    in  G[x]  \mleq{}  let  x  \mleftarrow{}{}  a
                        in  F[x]


By

---

Latex:
((RWO  "callbyvalueall-single"  0  THENA  Auto)
  THEN  SqLeTopToBase
  THEN  UseCbvaSqle
  THEN  BackThruSomeHyp)

---

Home Index