---

Step * of Lemma subtype_rel-tag-case

∀[T1,T2:Type]. ∀[z:Atom].  z:T1 ⊆r z:T2 supposing T1 ⊆r T2
BY
{ xxx(Unfold `tag-case` 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[z:Atom].    z:T1  \msubseteq{}r  z:T2  supposing  T1  \msubseteq{}r  T2


By

---

Latex:
xxx(Unfold  `tag-case`  0  THEN  Auto)xxx

---

Home Index