---

Step * of Lemma base-member-of-tagged+

∀[T,B:Type]. ∀[tg,a:Atom]. ∀[x:Base].
  (mk-tagged(tg;x) ∈ T |+ a:B) supposing ((¬(tg = a ∈ Atom)) and (mk-tagged(tg;x) ∈ T))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T,B:Type].  \mforall{}[tg,a:Atom].  \mforall{}[x:Base].
    (mk-tagged(tg;x)  \mmember{}  T  |+  a:B)  supposing  ((\mneg{}(tg  =  a))  and  (mk-tagged(tg;x)  \mmember{}  T))


By

---

Latex:
Auto

---

Home Index