---

Step * 1 2 of Lemma squash-per-class


1. T : Type
2. a1 : Base
3. b : Base
4. c : a1 = b ∈ T
⊢ (↓per-class(T;a1)) = (↓per-class(T;b)) ∈ Type
BY
{ RepeatFor 2 ((EqCD THEN Auto)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  Base
3.  b  :  Base
4.  c  :  a1  =  b
\mvdash{}  (\mdownarrow{}per-class(T;a1))  =  (\mdownarrow{}per-class(T;b))


By

---

Latex:
RepeatFor  2  ((EqCD  THEN  Auto))

---

Home Index