IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite-decidable-set1 1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. L:T List. x:T. P(x) (xL)
L:T List. x:T. P(x) (xL)
By:
RepeatFor 2 (ParallelOp -1) THEN BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:T. Dec(P(x))
L:T List. 
(x 
L)
