---

Step * of Lemma free-append-assoc

∀[X:Type]. ∀[x,y,z:free-word(X)].  (x + y + z = x + y + z ∈ free-word(X))
BY
{ (Auto THEN (Subst' x + y + z ~ x + y + z 0 THENM Auto)) }

1
.....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

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[x,y,z:free-word(X)].    (x  +  y  +  z  =  x  +  y  +  z)


By

---

Latex:
(Auto  THEN  (Subst'  x  +  y  +  z  \msim{}  x  +  y  +  z  0  THENM  Auto))

---

Home Index