(6steps total) PrintForm Definitions mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose bij
  T:Type, f,g:(TT). Bij(T; T; f)  Bij(T; T; g)  Bij(T; T; f o g)
By: Unfold `biject` 0 THEN Unfolds [`inject`;`surject`] 0 THEN Reduce 0

Generated subgoals:

1 1. T : Type
2. f : TT
3. g : TT
4. a1,a2:T. f(a1) = f(a2)  a1 = a2
5. b:T. a:T. f(a) = b
6. a1,a2:T. g(a1) = g(a2)  a1 = a2
7. b:T. a:T. g(a) = b
8. a1 : T
9. a2 : T
10. f(g(a1)) = f(g(a2))
  a1 = a2
1 step
2 1. T : Type
2. f : TT
3. g : TT
4. a1,a2:T. f(a1) = f(a2)  a1 = a2
5. b:T. a:T. f(a) = b
6. a1,a2:T. g(a1) = g(a2)  a1 = a2
7. b:T. a:T. g(a) = b
8. b : T
  a:T. f(g(a)) = b
4 steps

About:
applyfunctionuniverseequalimpliesallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) PrintForm Definitions mb list 2 Sections MarkB generic Doc