(4steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split int domain 1 1

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


By: BackThru: Hyp:3


Generated subgoals:

None

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

(4steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc