Nuprl - Proof: not over and

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: not over and

A,B:Prop. Dec(A)

(

(A & B)

By:

GenRepD

Generated subgoals:

1 1. A : Prop
2. B : Prop
3. Dec(A)
4. (A & B)
  A  B
4 steps

2 1. A : Prop
2. B : Prop
3. Dec(A)
4. A  B
  (A & B)
1 step

About:

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

1	1. A : Prop 2. B : Prop 3. Dec(A) 4. (A & B) A B	4 steps
2	1. A : Prop 2. B : Prop 3. Dec(A) 4. A B (A & B)	1 step