---

Step * 1 1 1 1 1 of Lemma fg-lift_wf


1. X : Type
2. G : Group{i}
3. f : X ⟶ |G|
4. (X + X) List ∈ Type
5. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
6. ∀w1:(X + X) List. word-equiv(X;w1;w1)
7. (X + X) List ∈ Type
8. ∀w3,w4:(X + X) List.  (word-equiv(X;w3;w4) ∈ Type)
9. ∀w3:(X + X) List. word-equiv(X;w3;w3)
10. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
11. w1 : (X + X) List
12. w2 : (X + X) List
13. word-equiv(X;w1;w2)
14. |G| = |G| ∈ Type
15. w3 : (X + X) List
16. w4 : (X + X) List
17. word-equiv(X;w3;w4)
18. |G| = |G| ∈ Type
⊢ fg-hom(G;f;w1 + w3) = fg-hom(G;f;w2 @ w4) ∈ |G|
BY
{ (Fold `free-append` 0 THEN RepeatFor 2 (EqCDA) THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  G  :  Group\{i\}
3.  f  :  X  {}\mrightarrow{}  |G|
4.  (X  +  X)  List  \mmember{}  Type
5.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
6.  \mforall{}w1:(X  +  X)  List.  word-equiv(X;w1;w1)
7.  (X  +  X)  List  \mmember{}  Type
8.  \mforall{}w3,w4:(X  +  X)  List.    (word-equiv(X;w3;w4)  \mmember{}  Type)
9.  \mforall{}w3:(X  +  X)  List.  word-equiv(X;w3;w3)
10.  EquivRel((X  +  X)  List;w1,w2.word-equiv(X;w1;w2))
11.  w1  :  (X  +  X)  List
12.  w2  :  (X  +  X)  List
13.  word-equiv(X;w1;w2)
14.  |G|  =  |G|
15.  w3  :  (X  +  X)  List
16.  w4  :  (X  +  X)  List
17.  word-equiv(X;w3;w4)
18.  |G|  =  |G|
\mvdash{}  fg-hom(G;f;w1  +  w3)  =  fg-hom(G;f;w2  @  w4)


By

---

Latex:
(Fold  `free-append`  0  THEN  RepeatFor  2  (EqCDA)  THEN  EqTypeCD  THEN  Auto)

---

Home Index