(3steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exist intseg null 1 1

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


By: Analyze-1


Generated subgoals:

None

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

(3steps total) PrintForm Definitions IteratedBinops Sections DiscrMathExt Doc