---

Step * of Lemma squash-per-class

∀[T:Type]. ∀[a:T].  (↓per-class(T;a))
BY
{ Auto }

1
1. T : Type
2. a : T
⊢ ↓per-class(T;a)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a:T].    (\mdownarrow{}per-class(T;a))


By

---

Latex:
Auto

---

Home Index