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