---

Step * of Lemma rec-value_subype_base

rec-value() ⊆r Base
BY
{ TACTIC:Assert ⌜∀n:ℕ. ∀v:rec-value().  ((rec-value-height(v) ≤ n) ⇒ (v ∈ Base))⌝⋅ }

1
.....assertion..... 
∀n:ℕ. ∀v:rec-value().  ((rec-value-height(v) ≤ n) ⇒ (v ∈ Base))

2
1. ∀n:ℕ. ∀v:rec-value().  ((rec-value-height(v) ≤ n) ⇒ (v ∈ Base))
⊢ rec-value() ⊆r Base

---

Latex:

---

Latex:
rec-value()  \msubseteq{}r  Base


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}v:rec-value().    ((rec-value-height(v)  \mleq{}  n)  {}\mRightarrow{}  (v  \mmember{}  Base))\mkleeneclose{}\mcdot{}

---

Home Index