---

Step * of Lemma RankEx4_ind_wf

∀[A:Type]. ∀[R:A ─→ RankEx4() ─→ ℙ]. ∀[v:RankEx4()]. ∀[Foo:foo:(ℤ + RankEx4())
                                                           ─→ case foo of inl(u) => True | inr(u1) => {x:A| R[x;u1]} 
                                                           ─→ {x:A| R[x;RankEx4_Foo(foo)]} ].
  (RankEx4_ind(v;
               RankEx4_Foo(foo)⇒ rec1.Foo[foo;rec1])  ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{RankEx4-definition:o, 1:l, i:l}⋅ }

---

Latex:


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


By

ProveDatatypeIndWf  TERMOF\{RankEx4-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index