---

Step * of Lemma usquash-elim

No Annotations
∀[T:ℙ]. (SqStable(T) ⇒ usquash(T) ⇒ T)
BY
{ (Intros THEN (Enough to prove ↓T  Because Auto) THEN UseWitness ⌜Ax⌝⋅ THEN UsquashElim (-1) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (Enough  to  prove  \mdownarrow{}T
                Because  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  UsquashElim  (-1)
  THEN  Auto)

---

Home Index