(9steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable ex int seg 1 1 3
1. i : 
2. j : 
3. F : {i..j}Prop
4. k:{i..j}. Dec(F(k))
5. ij
6. k:{...j}. ik  Dec(k:{k..j}. F(k))
  Dec(k:{i..j}. F(k))
By: BackThru: Hyp:-1

Generated subgoals:

None

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

(9steps total) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc