---

Step * of Lemma class-program-monotonic

∀[T,T':Type].  ClassProgram(T) ⊆r ClassProgram(T') supposing T ⊆r T'
BY
{ (Unfold `class-program` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,T':Type].    ClassProgram(T)  \msubseteq{}r  ClassProgram(T')  supposing  T  \msubseteq{}r  T'


By

---

Latex:
(Unfold  `class-program`  0  THEN  Auto)

---

Home Index