---

Step * 1 1 of Lemma free-append_wf


1. X : Type
2. w : w1,w2:(X + X) List//word-equiv(X;w1;w2)
3. (X + X) List ∈ Type
4. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
5. w' : w1,w2:(X + X) List//word-equiv(X;w1;w2)
6. w1 : (X + X) List@i
⊢ word-equiv(X;w1;w1)
BY
{ All Thin }

1
1. X : Type
2. w1 : (X + X) List@i
⊢ word-equiv(X;w1;w1)

---

Latex:

---

Latex:

1.  X  :  Type
2.  w  :  w1,w2:(X  +  X)  List//word-equiv(X;w1;w2)
3.  (X  +  X)  List  \mmember{}  Type
4.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
5.  w'  :  w1,w2:(X  +  X)  List//word-equiv(X;w1;w2)
6.  w1  :  (X  +  X)  List@i
\mvdash{}  word-equiv(X;w1;w1)


By

---

Latex:
All  Thin

---

Home Index