---

Step * 4 of Lemma radd-list-rabs

.....wf..... 
1. L : ℝ
2. L1 : ℝ List
⊢ istype(|radd-list(L1)| ≤ radd-list(map(λx.|x|;L1)))
BY
{ (RepeatFor 2 (TACTIC:MemCD') THEN Try (Complete (Auto)) THEN SubsumeC ⌜ℝ List⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  \mBbbR{}
2.  L1  :  \mBbbR{}  List
\mvdash{}  istype(|radd-list(L1)|  \mleq{}  radd-list(map(\mlambda{}x.|x|;L1)))


By

---

Latex:
(RepeatFor  2  (TACTIC:MemCD')  THEN  Try  (Complete  (Auto))  THEN  SubsumeC  \mkleeneopen{}\mBbbR{}  List\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index