(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Composing injections gives an injection.

At: comp preserves inj

  B,A,C:Type, g:(AB), f:(BC).
  Inj(A; B; g)  Inj(B; C; f)  Inj(A; C; f o g)
By: Def of Inj(<A>; <B>; <f>)

Generated subgoal:

1 1. B : Type
2. A : Type
3. C : Type
4. g : AB
5. f : BC
6. a1,a2:A. g(a1) = g(a2)  a1 = a2
7. b1,b2:B. f(b1) = f(b2)  b1 = b2
8. a1 : A
9. a2 : A
10. (f o g)(a1) = (f o g)(a2)
  a1 = a2
3 steps

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

(4steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc