PrintForm Definitions automata 5 Sections AutomataTheory Doc

At: surj is inj gen 1 1 1 1 1 1 1 1 1 1 1 1 1
1. A: Type
2. B: Type
3. f: AB
4. f1: AB
5. g: BA
6. InvFuns(A; B; f1; g)
7. n:
8. f2: nB
9. g1: Bn
10. InvFuns(n; B; f2; g1)
11. b: n
12. a: A
13. f(a) = f2(b)

(g1 o f o g o f2 o g1 o f1)(a) = b
By: Analyze 10
Generated subgoal:

110. g1 o f2 = Id
11. f2 o g1 = Id
12. b: n
13. a: A
14. f(a) = f2(b)
(g1 o f o g o f2 o g1 o f1)(a) = b

About:
equalnatural_numberapplyuniversefunction