Nuprl - Pf auto2_lemma

1. Alph: Type
2. n:
3. n1:
4. f: n1Alph
5. Bij(n1; Alph; f)
6. f:((nn1)(n1n)). Bij(nn1; (n1n); f)

f:((n1n){l:(Alph*)| ||l|| = n }). Bij((n1n); {l:(Alph*)| ||l|| = n }; f)

By: Inst Thm* (f:(AB). Bij(A; B; f)) (A ~ B) [nn1;(n1n)] THEN Analyze 7 THEN Thin 8 THEN Analyze 7

Generated subgoal:

1 7. (nn1) ~ (n1n)
f:((n1n){l:(Alph*)| ||l|| = n }). Bij((n1n); {l:(Alph*)| ||l|| = n }; f)

About: