---

Step * of Lemma sq_stable_usquash

No Annotations
∀[T:ℙ]. SqStable(usquash(T))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. [T] : ℙ
2. ↓usquash(T)
⊢ usquash(T)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index