---

Step * of Lemma mobj-ext

∀[L:MutualRectypeSpec]. mobj(L) ≡ i:Atom × mrec(L;i)
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. L : MutualRectypeSpec
2. x : i:Atom × mrec(L;i)
⊢ x ∈ mobj(L)

---

Latex:

---

Latex:
\mforall{}[L:MutualRectypeSpec].  mobj(L)  \mequiv{}  i:Atom  \mtimes{}  mrec(L;i)


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index