Step * of Lemma pi_term-induction

`∀[P:pi_term() ─→ ℙ]`
`  (P[pizero()]`
`  `` (∀pre:pi_prefix(). ∀body:pi_term().  (P[body] `` P[picomm(pre;body)]))`
`  `` (∀left,right:pi_term().  (P[left] `` P[right] `` P[pioption(left;right)]))`
`  `` (∀left,right:pi_term().  (P[left] `` P[right] `` P[pipar(left;right)]))`
`  `` (∀body:pi_term(). (P[body] `` P[pirep(body)]))`
`  `` (∀name:Name. ∀body:pi_term().  (P[body] `` P[pinew(name;body)]))`
`  `` {∀v:pi_term(). P[v]})`
BY
`{ ProveDatatypeInd }`

Latex:

Latex:
\mforall{}[P:pi\_term()  {}\mrightarrow{}  \mBbbP{}]
(P[pizero()]
{}\mRightarrow{}  (\mforall{}pre:pi\_prefix().  \mforall{}body:pi\_term().    (P[body]  {}\mRightarrow{}  P[picomm(pre;body)]))
{}\mRightarrow{}  (\mforall{}left,right:pi\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[pioption(left;right)]))
{}\mRightarrow{}  (\mforall{}left,right:pi\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[pipar(left;right)]))
{}\mRightarrow{}  (\mforall{}body:pi\_term().  (P[body]  {}\mRightarrow{}  P[pirep(body)]))
{}\mRightarrow{}  (\mforall{}name:Name.  \mforall{}body:pi\_term().    (P[body]  {}\mRightarrow{}  P[pinew(name;body)]))
{}\mRightarrow{}  \{\mforall{}v:pi\_term().  P[v]\})

By

Latex:
ProveDatatypeInd

Home Index