---

Step * of Lemma has-valueall-if-has-value-callbyvalueall

∀[a,b:Base].  has-valueall(a) supposing (let x ⟵ a in b[x])↓
BY
{ (Auto THEN UnfoldTopAb 0 THEN UnfoldAtAddr [1] (-1) THEN HasValueD (-1) THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    has-valueall(a)  supposing  (let  x  \mleftarrow{}{}  a  in  b[x])\mdownarrow{}


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0  THEN  UnfoldAtAddr  [1]  (-1)  THEN  HasValueD  (-1)  THEN  Trivial)

---

Home Index