---

Step * of Lemma coterm-size_wf

No Annotations
∀[opr:Type]. ∀[t:coterm(opr)].  (coterm-size(t) ∈ partial(ℕ))
BY
{ (Intros THEN Unhide) }

1
1. opr : Type
2. t : coterm(opr)
⊢ coterm-size(t) ∈ partial(ℕ)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[t:coterm(opr)].    (coterm-size(t)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
(Intros  THEN  Unhide)

---

Home Index