---

Step * 1 2 of Lemma mrec-lt_wf

.....subterm..... T:t
2:n
1. L : MutualRectypeSpec
2. x : mobj(L)
3. y : mobj(L)
⊢ x ∈ i:Atom × prec(lbl,p.mrec-spec(L;lbl;p);i)
BY
{ (Fold `mrec` 0 THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  L  :  MutualRectypeSpec
2.  x  :  mobj(L)
3.  y  :  mobj(L)
\mvdash{}  x  \mmember{}  i:Atom  \mtimes{}  prec(lbl,p.mrec-spec(L;lbl;p);i)


By

---

Latex:
(Fold  `mrec`  0  THEN  DoSubsume  THEN  Auto)

---

Home Index