(2steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star monotone 1
1. T : Type
2. R1 : TTProp
3. R2 : TTProp
4. R1 => R2
5. n : 
  R1^n => R2^n
By: BackThru Thm* n:, T:Type, R1,R2:(TTProp). R1 => R2  R1^n => R2^n

Generated subgoals:

None

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

(2steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc