---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index