At: auto2 lemma 7 1 1 1 1 1 2 1 2 1 1 1 1 1
1. Alph: Type
2. R: Alph*
Alph*Prop
3. n: 
4. L: Alph*
5. m:
6. 
x:Alph*. R(x,x)
7. x,y:Alph*. R(x,y) 
R(y,x)
8. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
9. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
10. 
w:(nAlph*). l:Alph*. i:n. R(l,w(i))
11. v: mAlph*
12. l:Alph*. L(l) 
(i:m. R(l,v(i)))
13. Fin(Alph)
14. x: Alph*
15. y: Alph*
16. l: Alph*
17. 
L(l @ x) = L(l @ y)
18. a': Alph*
19. ||a'|| < n
n
20. R((l @ x),a' @ x)
21. R((l @ y),a' @ y)
22. p: Alph*
23. q: Alph*
24. R(p,q)
25. L(p) (i:m. R(p,v(i)))
26. (L(p)) (i:m. R(p,v(i)))
27. L(q) (i:m. R(q,v(i)))
28. (L(q)) (i:m. R(q,v(i)))
L(p) = L(q)
By: Decide (L(p))
Generated subgoals:| 1 | 29. L(p)
L(p) = L(q) |
| 2 | 29. L(p)
L(p) = L(q) |
About:
