---

Step * 1 of Lemma has-value_functionality


1. a : Base
2. b : Base
3. a ≤ b
4. 0 ≤ eval a; 0
⊢ 0 ≤ eval b; 0
BY
{ (Using [`b',⌜eval a; 0⌝] (BLemma  `sqle_trans`)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Base
2.  b  :  Base
3.  a  \mleq{}  b
4.  0  \mleq{}  eval  a;  0
\mvdash{}  0  \mleq{}  eval  b;  0


By

---

Latex:
(Using  [`b',\mkleeneopen{}eval  a;  0\mkleeneclose{}]  (BLemma    `sqle\_trans`)\mcdot{}  THEN  Auto)

---

Home Index