---

Step * 1 of Lemma squash-per-class


1. T : Type
2. a : T
⊢ ↓per-class(T;a)
BY
{ PointwiseFunctionality 2 }

1
1. T : Type
2. [a1] : Base
3. [b] : Base
4. [c] : a1 = b ∈ T
⊢ ↓per-class(T;a1)

2
1. T : Type
2. a1 : Base
3. b : Base
4. c : a1 = b ∈ T
⊢ (↓per-class(T;a1)) = (↓per-class(T;b)) ∈ Type

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T
\mvdash{}  \mdownarrow{}per-class(T;a)


By

---

Latex:
PointwiseFunctionality  2

---

Home Index