---

Step * of Lemma usquash-equality

No Annotations
∀[T:ℙ]. ∀[S:Type].  usquash(T) = usquash(S) ∈ Type supposing ↓T ⇐⇒ ↓S
BY
{ (Auto THEN Unfold `usquash` 0) }

1
1. T : ℙ
2. S : Type
3. (↓T) ⇒ (↓S)
4. (↓T) ⇐ ↓S
⊢ pertype(λx,y. (↓T)) = pertype(λx,y. (↓S)) ∈ Type

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\mBbbP{}].  \mforall{}[S:Type].    usquash(T)  =  usquash(S)  supposing  \mdownarrow{}T  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}S


By

---

Latex:
(Auto  THEN  Unfold  `usquash`  0)

---

Home Index