---

Step * of Lemma RankEx4-induction

∀[P:RankEx4() ─→ ℙ]
  ((∀foo:ℤ + RankEx4(). (case foo of inl(u) => True | inr(u1) => P[u1] ⇒ P[RankEx4_Foo(foo)])) ⇒ {∀v:RankEx4(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[P:RankEx4()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}foo:\mBbbZ{}  +  RankEx4().  (case  foo  of  inl(u)  =>  True  |  inr(u1)  =>  P[u1]  {}\mRightarrow{}  P[RankEx4\_Foo(foo)]))
    {}\mRightarrow{}  \{\mforall{}v:RankEx4().  P[v]\})


By

ProveDatatypeInd

---

Home Index