---

Step * of Lemma callbyvalueall-single-sqle

∀[F,G:Base]. ∀[a:Top].  let x ⟵ a in F[x] ≤ let x ⟵ [a] in G[x] supposing ∀b:Base. (F[b] ≤ G[[b]])
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "callbyvalueall-single" 0 THENA Auto)
   THEN SqLeTopToBase
   THEN UseCbvaSqle
   THEN Try (BHyp 3 )
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,G:Base].  \mforall{}[a:Top].    let  x  \mleftarrow{}{}  a  in  F[x]  \mleq{}  let  x  \mleftarrow{}{}  [a]  in  G[x]  supposing  \mforall{}b:Base.  (F[b]  \mleq{}  G[[b]])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "callbyvalueall-single"  0  THENA  Auto)
  THEN  SqLeTopToBase
  THEN  UseCbvaSqle
  THEN  Try  (BHyp  3  )
  THEN  Auto)

---

Home Index