---

Step * of Lemma callbyvalueall-single-sqle2

∀[F,G:Base]. ∀[a:Top].  let x ⟵ [a] in G[x] ≤ let x ⟵ a in F[x] supposing ∀b:Base. (G[[b]] ≤ F[b])
BY
{ (UnivCD THENA Auto) }

1
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]

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index