---

Step * 1 1 1 of Lemma free-append_wf


1. X : Type
2. w1 : (X + X) List@i
⊢ word-equiv(X;w1;w1)
BY
{ (InstLemma `word-equiv-equiv` [⌜X⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  w1  :  (X  +  X)  List@i
\mvdash{}  word-equiv(X;w1;w1)


By

---

Latex:
(InstLemma  `word-equiv-equiv`  [\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index