---

Step * of Lemma pi_term_ind_wf_simple

∀[A:Type]. ∀[v:pi_term()]. ∀[zero:A]. ∀[comm:pre:pi_prefix() ⟶ body:pi_term() ⟶ A ⟶ A].
∀[option,par:left:pi_term() ⟶ right:pi_term() ⟶ A ⟶ A ⟶ A]. ∀[rep:body:pi_term() ⟶ A ⟶ A]. ∀[new:name:Name
                                                                                                       ⟶ body:pi_term()
                                                                                                       ⟶ A
                                                                                                       ⟶ A].
  (... ∈ A)
BY
{ ProveDatatypeIndWfSimple 0 `pi_term_ind_wf` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[v:pi\_term()].  \mforall{}[zero:A].  \mforall{}[comm:pre:pi\_prefix()  {}\mrightarrow{}  body:pi\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
\mforall{}[option,par:left:pi\_term()  {}\mrightarrow{}  right:pi\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[rep:body:pi\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
\mforall{}[new:name:Name  {}\mrightarrow{}  body:pi\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (...  \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  0  `pi\_term\_ind\_wf`

---

Home Index