---

Step * 1 of Lemma free-append-assoc

.....equality..... 
1. X : Type
2. x : free-word(X)
3. y : free-word(X)
4. z : free-word(X)
⊢ x + y + z ~ x + y + z
BY
{ (RepUR ``free-append`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  X  :  Type
2.  x  :  free-word(X)
3.  y  :  free-word(X)
4.  z  :  free-word(X)
\mvdash{}  x  +  y  +  z  \msim{}  x  +  y  +  z


By

---

Latex:
(RepUR  ``free-append``  0  THEN  Auto)

---

Home Index