---

Step * of Lemma subtype_rel_tagged+_general

∀[T,A,B:Type]. ∀[z:Atom].  (T ⊆r A |+ z:B) supposing ((T ⊆r z:B) and (T ⊆r A))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T,A,B:Type].  \mforall{}[z:Atom].    (T  \msubseteq{}r  A  |+  z:B)  supposing  ((T  \msubseteq{}r  z:B)  and  (T  \msubseteq{}r  A))


By

---

Latex:
Auto

---

Home Index