Nuprl - Pf one_one_preser

1. T: Type
2. S: Type
3. (n:, f:(nT). Bij(n; T; f)) & (f:(TS), g:(ST). InvFuns(T; S; f; g))

n:, f:(nS). Bij(n; S; f)

By: Analyze 3 THEN Analyze 3 THEN Analyze 4

Generated subgoal:

1 3. n:
4. f: nT
5. Bij(n; T; f)
6. f:(TS), g:(ST). InvFuns(T; S; f; g)
n:, f:(nS). Bij(n; S; f)

About: