---

Step * of Lemma has-value_functionality

∀[a,b:Base].  {(a)↓ ⇒ (b)↓} supposing a ≤ b
BY
{ (Auto THEN D 0 THEN Auto THEN ParallelLast) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  ParallelLast)

---

Home Index