Nuprl - Pf auto2_lemma_5 1 1 1 1 1 1 2 1 1 1 1

PrintForm Definitions exponent Sections AutomataTheory Doc

1. Alph: Type
2. n:
3. n1:
4. f: n1Alph
5. Bij(n1; Alph; f)
6. f:((nn1)(n1n)). 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 }

a1 = a2

By: ApFunToHypEquands `x' (i.x[i]) (nAlph) 12

Generated subgoals:

1 13. x: {l:(Alph*)| ||l|| = n }
14. i: n
i < ||x||

2 13. (i.((f o g(a1))[n])[i]) = (i.((f o g(a2))[n])[i]) nAlph
a1 = a2

About:

1	13. `x:` `{l:(Alph*)\| \|\|l\|\| = n }` 14. `i:` `n` `i < \|\|x\|\|`
2	13. `(i.((f o g(a1))[n])[i]) = (i.((f o g(a2))[n])[i]) nAlph` `a1 = a2`