---

Step * of Lemma pi_prefix-definition

∀[A:Type]. ∀[R:A ⟶ pi_prefix() ⟶ ℙ].
  ((∀chan,var:Name.  {x:A| R[x;pisend(chan;var)]} )
  ⇒ (∀chan,var:Name.  {x:A| R[x;pircv(chan;var)]} )
  ⇒ {∀v:pi_prefix(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `pi_prefix-induction` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  pi\_prefix()  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}chan,var:Name.    \{x:A|  R[x;pisend(chan;var)]\}  )
    {}\mRightarrow{}  (\mforall{}chan,var:Name.    \{x:A|  R[x;pircv(chan;var)]\}  )
    {}\mRightarrow{}  \{\mforall{}v:pi\_prefix().  \{x:A|  R[x;v]\}  \})


By

---

Latex:
ProveDatatypeDefinition  `pi\_prefix-induction`

---

Home Index