PrintForm Definitions finite sets Sections AutomataTheory Doc

At: one2one preserves fin 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
1. T: Type
2. U: Type
3. f: TU
4. g: UT
5. g o f = Id
6. f o g = Id
7. n:
8. f1: nT
9. Inj(n; T; f1)
10. Surj(n; T; f1)
11. a1: n
12. a2: n
13. (f o f1)(a1) = (f o f1)(a2)
14. (g o f o f1)(a1) = (g o f o f1)(a2)

a1 = a2
By: RWH (LemmaC Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD) 14
Generated subgoal:

114. (g o f o f1)(a1) = (g o f o f1)(a2)
a1 = a2

About:
equalnatural_numberuniversefunctionapply