---

Step * of Lemma free-word-inv-append1

∀[X:Type]. ∀[x:free-word(X)].  (free-word-inv(x) + x = 0 ∈ free-word(X))
BY
{ (Auto
   THEN (InstLemma `word-equiv-equiv` [⌜X⌝]⋅ THEN Auto)
   THEN (newQuotientElim 2 ⋅ THENA Auto)
   THEN (Assert ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List) BY
               (RepUR ``free-word-inv`` 0 THEN Auto))
   THEN EqTypeCD
   THEN Auto
   THEN RepUR ``free-append free-0`` 0
   THEN Auto
   THEN D 0 With ⌜[]⌝ 
   THEN Auto) }

1
1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. word-equiv(X;w1;w2)
9. free-word(X) = free-word(X) ∈ Type
10. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
⊢ λx,y. word-rel(X;x;y)^* (free-word-inv(w1) @ w1) []

2
1. X : Type
2. (X + X) List ∈ Type
3. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
4. ∀w1:(X + X) List. word-equiv(X;w1;w1)
5. EquivRel((X + X) List;w1,w2.word-equiv(X;w1;w2))
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. word-equiv(X;w1;w2)
9. free-word(X) = free-word(X) ∈ Type
10. ∀w:(X + X) List. (free-word-inv(w) ∈ (X + X) List)
11. λx,y. word-rel(X;x;y)^* (free-word-inv(w1) @ w1) []
⊢ λx,y. word-rel(X;x;y)^* [] []

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[x:free-word(X)].    (free-word-inv(x)  +  x  =  0)


By

---

Latex:
(Auto
  THEN  (InstLemma  `word-equiv-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (newQuotientElim  2  \mcdot{}  THENA  Auto)
  THEN  (Assert  \mforall{}w:(X  +  X)  List.  (free-word-inv(w)  \mmember{}  (X  +  X)  List)  BY
                          (RepUR  ``free-word-inv``  0  THEN  Auto))
  THEN  EqTypeCD
  THEN  Auto
  THEN  RepUR  ``free-append  free-0``  0
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}[]\mkleeneclose{} 
  THEN  Auto)

---

Home Index