---

Step * of Lemma eval-list-sq

∀[L:ℤ List]. (eval-list(L) ~ L)
BY
{ ((D 0 THENA Auto) THEN (Assert SQType(ℤ List) BY SqTac)) }

1
1. L : ℤ List
2. SQType(ℤ List)
⊢ eval-list(L) ~ L

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  (eval-list(L)  \msim{}  L)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (Assert  SQType(\mBbbZ{}  List)  BY  SqTac))

---

Home Index