(4steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: compose-biject
A,B,C:Type, f:(AB), g:(BC). Bij(A; B; f) Bij(B; C; g) Bij(A; C; g o f)
By:
Unfold `biject` 0
THEN
Unfolds [`inject`;`surject`] 0
THEN
Reduce 0
Generated subgoals:

11. A: Type
2. B: Type
3. C: Type
4. f: AB
5. g: BC
6. a1,a2:A. f(a1) = f(a2) a1 = a2
7. b:B. a:A. f(a) = b
8. a1,a2:B. g(a1) = g(a2) a1 = a2
9. b:C. a:B. g(a) = b
10. a1: A
11. a2: A
12. g(f(a1)) = g(f(a2))
a1 = a2		1 step
 
21. A: Type
2. B: Type
3. C: Type
4. f: AB
5. g: BC
6. a1,a2:A. f(a1) = f(a2) a1 = a2
7. b:B. a:A. f(a) = b
8. a1,a2:B. g(a1) = g(a2) a1 = a2
9. b:C. a:B. g(a) = b
10. b: C
a:A. g(f(a)) = b		2 steps

About:
applyfunctionuniverseequalimpliesallexists

(4steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc