---

Step * of Lemma ball_nil_lemma

∀f,T:Top.  (∀bx(:T) ∈ []. f[x] ~ tt)
BY
{ ((UnivCD THENA Auto) THEN Unfold `ball` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f,T:Top.    (\mforall{}\msubb{}x(:T)  \mmember{}  [].  f[x]  \msim{}  tt)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `ball`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index