---

Step * 1 of Lemma map-conversion-test


1. T : Type
2. T ⊆r Base
3. L : T List List
⊢ map(λX.(X @ []);L) ~ map(λX.X;L)
BY
{  let C = SweepDnC (LemmaC `append-nil`) in 
      RW (SweepDnC (MapSqC C)) 0⋅ }

1
1. T : Type
2. T ⊆r Base
3. L : T List List
⊢ map(λX.X;L) ~ map(λX.X;L)

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  L  :  T  List  List
\mvdash{}  map(\mlambda{}X.(X  @  []);L)  \msim{}  map(\mlambda{}X.X;L)


By

---

Latex:
  let  C  =  SweepDnC  (LemmaC  `append-nil`)  in 
            RW  (SweepDnC  (MapSqC  C))  0\mcdot{}

---

Home Index