---

Step * 1 1 of Lemma map-conversion-test2


1. L : ℤ List
2. ∀x:ℤ. (x + 0 ~ x)
⊢ map(λx.(x + 0);L) ~ map(λx.x;L)
BY
{ TACTIC:RW (SweepDnC (MapSqC (SweepDnC (HypC 2)))) 0⋅ .... }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:RW  (SweepDnC  (MapSqC  (SweepDnC  (HypC  2))))  0\mcdot{}  ....

---

Home Index