---

Step * of Lemma free-append-0

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[w:free-word(X)].    (w  +  0  =  w)


By

---

Latex:
(Auto
  THEN  (newQuotientElim  2  \mcdot{}  THENA  Auto)
  THEN  InstLemma  `word-equiv-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  EqTypeCD
  THEN  Auto
  THEN  RepUR  ``free-append  free-0``  0
  THEN  Auto)

---

Home Index