---

Step * of Lemma usquash-implies-squash

No Annotations
∀[T:ℙ]. (usquash(T) ⇒ (↓T))
BY
{ ((Auto THEN UsquashElim (-1)) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbP{}].  (usquash(T)  {}\mRightarrow{}  (\mdownarrow{}T))


By

---

Latex:
((Auto  THEN  UsquashElim  (-1))  THEN  Auto)

---

Home Index