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

At: compose-biject 2
1. 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
By:
InstHyp [b] -2
THEN
ExRepD
THEN
InstHyp [a] -6
THEN
ParallelOp -1
Generated subgoal:

111. a: B
12. g(a) = b
13. a@0: A
14. f(a@0) = a
g(f(a@0)) = b		1 step

About:
applyfunctionuniverseequalimpliesallexists

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