---

Step * of Lemma RankEx4_Foo-foo_wf

∀[v:RankEx4()]. RankEx4_Foo-foo(v) ∈ ℤ + RankEx4() supposing ↑RankEx4_Foo?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[v:RankEx4()].  RankEx4\_Foo-foo(v)  \mmember{}  \mBbbZ{}  +  RankEx4()  supposing  \muparrow{}RankEx4\_Foo?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index