---

Step * 1 1 of Lemma squash-per-class


1. T : Type
2. [a1] : Base
3. [b] : Base
4. [c] : a1 = b ∈ T
⊢ ↓per-class(T;a1)
BY
{ (Unhide THEN D 0 THEN UseWitness ⌜a1⌝⋅ THEN MemTypeCD THEN Try (BLemma `equal-wf-base-T`) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Unhide  THEN  D  0  THEN  UseWitness  \mkleeneopen{}a1\mkleeneclose{}\mcdot{}  THEN  MemTypeCD  THEN  Try  (BLemma  `equal-wf-base-T`)  THEN  Auto)

---

Home Index