IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
dec pred iff some boolfun2 1. T : Type
2. E : TProp
3. f:(T). x:T. f(x) E(x)
4. x : T Dec(E(x))
By:
Analyze-2 THEN Rewrite by Hyp:-2
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
f:(T
). 
x:T. f(x) 
E(x)
Dec(E(x))
