---

Step * 2 of Lemma rec-value_subype_base


1. ∀n:ℕ. ∀v:rec-value().  ((rec-value-height(v) ≤ n) ⇒ (v ∈ Base))
⊢ rec-value() ⊆r Base
BY
{ TACTIC:((D 0 THENA Auto) THEN InstHyp [⌜rec-value-height(x)⌝;⌜x⌝] 1⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}n:\mBbbN{}.  \mforall{}v:rec-value().    ((rec-value-height(v)  \mleq{}  n)  {}\mRightarrow{}  (v  \mmember{}  Base))
\mvdash{}  rec-value()  \msubseteq{}r  Base


By

---

Latex:
TACTIC:((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}rec-value-height(x)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THEN  Auto)

---

Home Index