---

Step * 1 of Lemma free-append_wf


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)
BY
{ (newQuotientElim 3 ⋅ THENA Auto) }

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

2
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. ∀w1:(X + X) List. word-equiv(X;w1;w1)
6. w1 : (X + X) List@i
7. w2 : (X + X) List@i
8. word-equiv(X;w1;w2)
9. (w1,w2:(X + X) List//word-equiv(X;w1;w2)) = (w1,w2:(X + X) List//word-equiv(X;w1;w2)) ∈ Type
⊢ w + w1 = w + w2 ∈ (w1,w2:(X + X) List//word-equiv(X;w1;w2))

---

Latex:

---

Latex:

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)
\mvdash{}  w  +  w'  \mmember{}  w1,w2:(X  +  X)  List//word-equiv(X;w1;w2)


By

---

Latex:
(newQuotientElim  3  \mcdot{}  THENA  Auto)

---

Home Index