Nuprl - Proof: negnegelim vs bivalence

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Double negation elimination is equivalent to bivalence.

(

P:Prop.

(

P:Prop. P

By:

Auto

Generated subgoals:

1 1. P:Prop. P  P
2. P : Prop
  P  P
7 steps

2 1. P:Prop. P  P
2. P : Prop
3. P
  P
4 steps

About:

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

1	1. P:Prop. P P 2. P : Prop P P	7 steps
2	1. P:Prop. P P 2. P : Prop 3. P P	4 steps