---

Step * 1 1 1 1 2 1 1 1 of Lemma free-group-generators


1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
8. (X + X) List ∈ Type
9. w : (X + X) List@i
10. ∀[a:free-word(X)]. ((f free-word-inv(a)) = (~ (f a)) ∈ |G|)
11. ∀[a:free-word(X)]. ((g free-word-inv(a)) = (~ (g a)) ∈ |G|)
⊢ (f w) = (g w) ∈ |G|
BY
{ ListInd (-3)⋅ }

1
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
8. (X + X) List ∈ Type
9. ∀[a:free-word(X)]. ((f free-word-inv(a)) = (~ (f a)) ∈ |G|)
10. ∀[a:free-word(X)]. ((g free-word-inv(a)) = (~ (g a)) ∈ |G|)
⊢ (f []) = (g []) ∈ |G|

2
1. X : Type
2. G : Group{i}@i'
3. f : |free-group(X)| ⟶ |G|
4. IsMonHom{free-group(X),G}(f)
5. g : |free-group(X)| ⟶ |G|
6. IsMonHom{free-group(X),G}(g)
7. ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
8. (X + X) List ∈ Type
9. ∀[a:free-word(X)]. ((f free-word-inv(a)) = (~ (f a)) ∈ |G|)
10. ∀[a:free-word(X)]. ((g free-word-inv(a)) = (~ (g a)) ∈ |G|)
11. u : X + X@i
12. v : (X + X) List@i
13. (f v) = (g v) ∈ |G|
⊢ (f [u / v]) = (g [u / v]) ∈ |G|

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}@i'
3.  f  :  |free-group(X)|  {}\mrightarrow{}  |G|
4.  IsMonHom\{free-group(X),G\}(f)
5.  g  :  |free-group(X)|  {}\mrightarrow{}  |G|
6.  IsMonHom\{free-group(X),G\}(g)
7.  \mforall{}x:X.  ((f  free-letter(x))  =  (g  free-letter(x)))
8.  (X  +  X)  List  \mmember{}  Type
9.  w  :  (X  +  X)  List@i
10.  \mforall{}[a:free-word(X)].  ((f  free-word-inv(a))  =  (\msim{}  (f  a)))
11.  \mforall{}[a:free-word(X)].  ((g  free-word-inv(a))  =  (\msim{}  (g  a)))
\mvdash{}  (f  w)  =  (g  w)


By

---

Latex:
ListInd  (-3)\mcdot{}

---

Home Index