---

Step * of Lemma RankEx4_Foo_wf

∀[foo:ℤ + RankEx4()]. (RankEx4_Foo(foo) ∈ RankEx4())
BY
{ DepprodCoDatatypeConstructorWf `RankEx4_size` }

---

Latex:

---

Latex:
\mforall{}[foo:\mBbbZ{}  +  RankEx4()].  (RankEx4\_Foo(foo)  \mmember{}  RankEx4())


By

---

Latex:
DepprodCoDatatypeConstructorWf  `RankEx4\_size`

---

Home Index