PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun preserves fin 1 1 1 1 1
1. S: Type
2. T: Type
3. (n:, f:(nS), g:(Sn). g o f = Id & f o g = Id) & (n:, f:(nT), g:(Tn). g o f = Id & f o g = Id)

n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id
By:
Analyze 3
THEN
Analyze 3
Generated subgoal:

13. n:
4. f:(nS), g:(Sn). g o f = Id & f o g = Id
5. n:, f:(nT), g:(Tn). g o f = Id nn & f o g = Id
n:, f:(nST), g:((ST)n). g o f = Id nn & f o g = Id

About:
existsfunctionnatural_numberandequaluniverse