---

Step * of Lemma RankEx4_ind_wf_simple

∀[A:Type]. ∀[v:RankEx4()]. ∀[Foo:foo:(ℤ + RankEx4()) ⟶ case foo of inl(u) => True | inr(u1) => A ⟶ A].
  (RankEx4_ind(v;
               RankEx4_Foo(foo)⇒ rec1.Foo[foo;rec1])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 0 `RankEx4_ind_wf` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[v:RankEx4()].  \mforall{}[Foo:foo:(\mBbbZ{}  +  RankEx4())
                                                                  {}\mrightarrow{}  case  foo  of  inl(u)  =>  True  |  inr(u1)  =>  A
                                                                  {}\mrightarrow{}  A].
    (RankEx4\_ind(v;
                              RankEx4\_Foo(foo){}\mRightarrow{}  rec1.Foo[foo;rec1])    \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  0  `RankEx4\_ind\_wf`

---

Home Index