---

Step * 1 of Lemma sparse-signed-rep_wf


1. v : {-1..2-} List
⊢ evalall(v) ~ v
BY
{ xxx(BLemma `evalall-reduce` THEN Auto)xxx }

---

Latex:

---

Latex:

1.  v  :  \{-1..2\msupminus{}\}  List
\mvdash{}  evalall(v)  \msim{}  v


By

---

Latex:
xxx(BLemma  `evalall-reduce`  THEN  Auto)xxx

---

Home Index