---

Step * 1 2 1 of Lemma free-append_wf


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))
BY
{ (EqTypeCD THEN Auto THEN RepUR ``free-append`` 0 THEN 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
⊢ word-equiv(X;w3 @ w1;w4 @ w2)

---

Latex:

---

Latex:

1.  X  :  Type
2.  (X  +  X)  List  \mmember{}  Type
3.  \mforall{}w3,w4:(X  +  X)  List.    (word-equiv(X;w3;w4)  \mmember{}  Type)
4.  \mforall{}w3:(X  +  X)  List.  word-equiv(X;w3;w3)
5.  (X  +  X)  List  \mmember{}  Type
6.  \mforall{}w1,w2:(X  +  X)  List.    (word-equiv(X;w1;w2)  \mmember{}  Type)
7.  \mforall{}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))
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))
\mvdash{}  w3  +  w1  =  w4  +  w2


By

---

Latex:
(EqTypeCD  THEN  Auto  THEN  RepUR  ``free-append``  0  THEN  Auto)

---

Home Index