Nuprl - Proof: decidable functionality

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable functionality

P,Q:Prop. (P

(Dec(P)

Dec(Q))

By:

GenUnivCD

Generated subgoals:

1 1. P : Prop
2. Q : Prop
3. P  Q
4. Dec(P)
  Dec(Q)
1 step

2 1. P : Prop
2. Q : Prop
3. P  Q
4. Dec(Q)
  Dec(P)
3 steps

About:

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

1	1. P : Prop 2. Q : Prop 3. P Q 4. Dec(P) Dec(Q)	1 step
2	1. P : Prop 2. Q : Prop 3. P Q 4. Dec(Q) Dec(P)	3 steps