---

Step * of Lemma eval-mklist_wf

∀[T:Type]. ∀[n,offset:ℕ]. ∀[f:{offset..n + offset-} ⟶ T].  (eval-mklist(n;f;offset) ∈ T List) supposing value-type(T)
BY
{ (Auto THEN RWO  "eval-mklist-sq" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[n,offset:\mBbbN{}].  \mforall{}[f:\{offset..n  +  offset\msupminus{}\}  {}\mrightarrow{}  T].    (eval-mklist(n;f;offset)  \mmember{}  T  List) 
    supposing  value-type(T)


By

---

Latex:
(Auto  THEN  RWO    "eval-mklist-sq"  0  THEN  Auto)

---

Home Index