∀[L:MutualRectypeSpec]. mobj(L) ≡ i:Atom × mrec(L;i)
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }
.....subterm..... T:t
1:n
1. L : MutualRectypeSpec
2. x : i:Atom × mrec(L;i)
⊢ x ∈ mobj(L)