(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. 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 : 
  P(a,b)


By: Decide: ba


Generated subgoals:

1 6. ba
  P(a,b)

1 step
2 6. ba
  P(a,b)

2 steps

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

(5steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc