(5steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all int pairs via all splits 1 1

1. P : Prop
2. a:b:{...a}. P(a,b)
3. a:. (b:{...a}. P(a,b))  (b:{a...}. P(a,b))
4. a : 
5. b : 
6. ba
  P(a,b)


By: BackThru: Hyp:2


Generated subgoals:

None

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

(5steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc