---

Step * of Lemma has-valueall-apply

∀[a,g:Base].  has-valueall(g) supposing has-valueall(g a)
BY
{ (Auto
   THEN Unfold `has-valueall` 0
   THEN (Auto THEN Fold `has-valueall` 0)
   THEN FLemma `has-valueall-has-value` [-1]
   THEN Auto
   THEN HasValueD (-1)) }

1
1. a : Base
2. g : Base
3. has-valueall(g a)
4. (g a)↓
5. (g)↓
⊢ has-valueall(g)

---

Latex:

---

Latex:
\mforall{}[a,g:Base].    has-valueall(g)  supposing  has-valueall(g  a)


By

---

Latex:
(Auto
  THEN  Unfold  `has-valueall`  0
  THEN  (Auto  THEN  Fold  `has-valueall`  0)
  THEN  FLemma  `has-valueall-has-value`  [-1]
  THEN  Auto
  THEN  HasValueD  (-1))

---

Home Index