(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose wf inj
  A,B,C:Type, f:(B inj C), g:(A inj B). f o g  A inj C
By: UnivCD THEN Analyze-1 THEN Analyze4 THEN Analyze

Generated subgoal:

1 1. A : Type
2. B : Type
3. C : Type
4. f : BC
5. Inj(B; C; f)
6. g : AB
7. Inj(A; B; g)
  Inj(A; C; f o g)
1 step

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

(2steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc