---

Step * of Lemma l_treeco_size_wf

∀[L,T:Type]. ∀[p:l_treeco(L;T)].  (l_treeco_size(p) ∈ partial(ℕ))
BY
{ ProveCoSizeWf }

---

Latex:


\mforall{}[L,T:Type].  \mforall{}[p:l\_treeco(L;T)].    (l\_treeco\_size(p)  \mmember{}  partial(\mBbbN{}))


By

ProveCoSizeWf

---

Home Index