---

Step * 1 of Lemma map-conversion-test2


1. L : ℤ List
⊢ map(λx.(x + 0);L) ~ map(λx.x;L)
BY
{ TACTIC:(Assert ∀x:ℤ. (x + 0 ~ x) BY
                Auto) }

1
1. L : ℤ List
2. ∀x:ℤ. (x + 0 ~ x)
⊢ map(λx.(x + 0);L) ~ map(λx.x;L)

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
\mvdash{}  map(\mlambda{}x.(x  +  0);L)  \msim{}  map(\mlambda{}x.x;L)


By

---

Latex:
TACTIC:(Assert  \mforall{}x:\mBbbZ{}.  (x  +  0  \msim{}  x)  BY
                            Auto)

---

Home Index