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