At: auto2 lemma 5 1 1 1 1 1 1 2 2 1 1 1 1 1 2 1 1 1 2 1 2
1. Alph: Type
2. n: 
3. n1:
4. f: n1
Alph
5. Bij(n1; Alph; f)
6. 
f:((nn1)(n1
n)). Bij(nn1; (n1n); f)
7. f1: (nn1)(n1n)
8. g: (n1n)nn1
9. InvFuns(nn1; (n1n); f1; g)
10. b: {l:(Alph*)| ||l|| = n }
11. g1: Alphn1
12. g1 o f = Id
13. f o g1 = Id
14. a: (n1n)
15. g(a) = g1 o (
z:||b||. b[z]) 
nn1
16. f o g(a) = Id o (z:||b||. b[z]) nAlph
f o g(a) = (z:||b||. b[z]) nAlph
By: RWH
(LemmaC
Thm* 
f:(AB). Id o f = f)
16
Generated subgoal:| 1 | 17. z: n
z < ||b|| |
About:
