---

Step * 2 3 1 of Lemma free-group-functor_wf


1. X : Type@i'
2. Y : Type@i'
3. z : Type@i'
4. f : X ⟶ Y@i'
5. g : Y ⟶ z@i'
6. x : X@i
⊢ free-letter(g (f x)) = free-letter(g (f x)) ∈ free-word(z)
BY
{ Auto }

---

Latex:

---

Latex:

1.  X  :  Type@i'
2.  Y  :  Type@i'
3.  z  :  Type@i'
4.  f  :  X  {}\mrightarrow{}  Y@i'
5.  g  :  Y  {}\mrightarrow{}  z@i'
6.  x  :  X@i
\mvdash{}  free-letter(g  (f  x))  =  free-letter(g  (f  x))


By

---

Latex:
Auto

---

Home Index