PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun preserves fin 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
1. S: Type
2. T: Type
3. n:
4. f: nS
5. g: Sn
6. g o f = Id
7. f o g = Id
8. n1:
9. f1: n1T
10. g1: Tn1
11. g1 o f1 = Id
12. f1 o g1 = Id
13. f2: (nn1)(n1n)
14. g2: (n1n)nn1
15. g2 o f2 = Id
16. f2 o g2 = Id
17. x: (n1n)

(x@0.g2(x,x@0)) = g2(x)
By: Ext
Generated subgoal:

118. x1: n
(x@0.g2(x,x@0))(x1) = g2(x,x1)

About:
equalfunctionnatural_numberlambdaapplyuniverse