---

Step * of Lemma RankEx4-definition

∀[A:Type]. ∀[R:A ─→ RankEx4() ─→ ℙ].
  ((∀foo:ℤ + RankEx4(). (case foo of inl(u) => True | inr(u1) => {x:A| R[x;u1]}  ⇒ {x:A| R[x;RankEx4_Foo(foo)]} ))
  ⇒ {∀v:RankEx4(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `RankEx4-induction` }

---

Latex:


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


By

ProveDatatypeDefinition  `RankEx4-induction`

---

Home Index