---

Step * of Lemma map-permute_list

∀[g:Top]. ∀[L:Top List]. ∀[f:ℕ||L|| ⟶ ℕ||L||].  (map(g;(L o f)) ~ (map(g;L) o f))
BY
{ xxxAutoxxx }

1
1. g : Top
2. L : Top List
3. f : ℕ||L|| ⟶ ℕ||L||
⊢ map(g;(L o f)) ~ (map(g;L) o f)

---

Latex:

---

Latex:
\mforall{}[g:Top].  \mforall{}[L:Top  List].  \mforall{}[f:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||].    (map(g;(L  o  f))  \msim{}  (map(g;L)  o  f))


By

---

Latex:
xxxAutoxxx

---

Home Index