At: auto2 lemma 7 1 1 2 1 3
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*). l:Alph*. L(l) 
(i:m. R(l,v(i)))
12. Fin(Alph)
13. x: Alph*
14. y: Alph*
15. (l:Alph*. 
L(l @ x) = L(l @ y)) (k:(n
n), l:{l:(Alph*)| ||l|| = k 
}. L(l @ x) = L(l @ y))
16. Dec(t:(nn). (
k.l:{l:(Alph*)| ||l|| = k }. L(l @ x) = L(l @ y) )(t))
Dec(k:(nn), l:{l:(Alph*)| ||l|| = k }. L(l @ x) = L(l @ y))
By: Reduce 16
Generated subgoals:None
About:
