---

Step * 1 2 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. ∀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))
BY
{ (newQuotientElim 2 ⋅ THENA Auto) }

1
1. X : Type
2. (X + X) List ∈ Type
3. ∀w3,w4:(X + X) List.  (word-equiv(X;w3;w4) ∈ Type)
4. ∀w3:(X + X) List. word-equiv(X;w3;w3)
5. (X + X) List ∈ Type
6. ∀w1,w2:(X + X) List.  (word-equiv(X;w1;w2) ∈ Type)
7. ∀w1:(X + X) List. word-equiv(X;w1;w1)
8. w1 : (X + X) List@i
9. w2 : (X + X) List@i
10. word-equiv(X;w1;w2)
11. (w1,w2:(X + X) List//word-equiv(X;w1;w2)) = (w1,w2:(X + X) List//word-equiv(X;w1;w2)) ∈ Type
12. w3 : (X + X) List@i
13. w4 : (X + X) List@i
14. word-equiv(X;w3;w4)
15. (w1,w2:(X + X) List//word-equiv(X;w1;w2)) = (w1,w2:(X + X) List//word-equiv(X;w1;w2)) ∈ Type
⊢ w3 + w1 = w4 + 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.  (X  +  X)  List  \mmember{}  Type
4.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
5.  \mforall{}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))
\mvdash{}  w  +  w1  =  w  +  w2


By

---

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

---

Home Index