---

Step * of Lemma free-append_wf

∀[X:Type]. ∀[w,w':free-word(X)].  (w + w' ∈ free-word(X))
BY
{ (Auto THEN All (Unfold `free-word`)) }

1
1. X : Type
2. w : w1,w2:(X + X) List//word-equiv(X;w1;w2)
3. w' : w1,w2:(X + X) List//word-equiv(X;w1;w2)
⊢ w + w' ∈ w1,w2:(X + X) List//word-equiv(X;w1;w2)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[w,w':free-word(X)].    (w  +  w'  \mmember{}  free-word(X))


By

---

Latex:
(Auto  THEN  All  (Unfold  `free-word`))

---

Home Index