---

Step * of Lemma has-valueall-single

∀[a:Base]. uiff(has-valueall(a);has-valueall([a]))
BY
{ Auto }

1
1. a : Base
2. has-valueall(a)
⊢ has-valueall([a])

2
1. a : Base
2. has-valueall([a])
⊢ has-valueall(a)

---

Latex:

---

Latex:
\mforall{}[a:Base].  uiff(has-valueall(a);has-valueall([a]))


By

---

Latex:
Auto

---

Home Index