---

Step * of Lemma mrec-induction2

∀L:MutualRectypeSpec. ∀[P:mobj(L) ⟶ TYPE]. (mrecind(L;x.P[x]) ⇒ (∀x:mobj(L). P[x]))
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. L : MutualRectypeSpec
2. [P] : mobj(L) ⟶ TYPE
3. mrecind(L;x.P[x])
⊢ ∀x:mobj(L). P[x]

---

Latex:

---

Latex:
\mforall{}L:MutualRectypeSpec.  \mforall{}[P:mobj(L)  {}\mrightarrow{}  TYPE].  (mrecind(L;x.P[x])  {}\mRightarrow{}  (\mforall{}x:mobj(L).  P[x]))


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index