At: auto2 lemma 5 1 1 1 1 1 1 2 1 1 1 1 1
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. a1: (n1n)
11. a2: (n1n)
12. ((f o g(a1))[n]) = ((f o g(a2))[n]) 
{l:(Alph*)| ||l|| = n }
13. x: {l:(Alph*)| ||l|| = n }
14. i: n
i < ||x||
By: Analyze 13
Generated subgoals:None
About:
