---

Step * of Lemma has-value-monotonic

∀[a,b:Base].  ((b)↓) supposing ((a ≤ b) and (a)↓)
BY
{ (Auto THEN All (Unfold `has-value`)) }

1
1. a : Base
2. b : Base
3. 0 ≤ eval a; 0
4. a ≤ b
⊢ 0 ≤ eval b; 0

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    ((b)\mdownarrow{})  supposing  ((a  \mleq{}  b)  and  (a)\mdownarrow{})


By

---

Latex:
(Auto  THEN  All  (Unfold  `has-value`))

---

Home Index