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 1 1 1 1 1
1. A: Type
2. B: Type
3. f: AB
4. f1: AB
5. g: BA
6. g o f1 = Id
7. f1 o g = Id
8. n:
9. f2: nB
10. g1: Bn
11. g1 o f2 = Id
12. f2 o g1 = Id
13. b: n
14. a: A
15. f(a) = f2(b)
16. g1(f(a)) = g1(f2(b))

g1(f(a)) = b
By: RW (AddrC [3] add_composeC) 16
Generated subgoal:

116. g1(f(a)) = (g1 o f2)(b)
g1(f(a)) = b

About:
equalnatural_numberapplyuniversefunction