(15steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable vs unique nsub2 1
1. P : Prop
  Dec(P)  (!i:2. if i=0 P else P fi)
By: GenUnivCD

Generated subgoals:

1 2. Dec(P)
  !i:2. if i=0 P else P fi
9 steps
2 2. !i:2. if i=0 P else P fi
  Dec(P)
4 steps

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

(15steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc