---

Step * of Lemma pi_term-definition

∀[A:Type]. ∀[R:A ⟶ pi_term() ⟶ ℙ].
  ({x:A| R[x;pizero()]} 
  ⇒ (∀pre:pi_prefix(). ∀body:pi_term().  ({x:A| R[x;body]}  ⇒ {x:A| R[x;picomm(pre;body)]} ))
  ⇒ (∀left,right:pi_term().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;pioption(left;right)]} ))
  ⇒ (∀left,right:pi_term().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;pipar(left;right)]} ))
  ⇒ (∀body:pi_term(). ({x:A| R[x;body]}  ⇒ {x:A| R[x;pirep(body)]} ))
  ⇒ (∀name:Name. ∀body:pi_term().  ({x:A| R[x;body]}  ⇒ {x:A| R[x;pinew(name;body)]} ))
  ⇒ {∀v:pi_term(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `pi_term-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `pi\_term-induction`

---

Home Index