Nuprl - Proof: card split decbl squash

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card split decbl squash

A:Type, P:(A

Prop).

(

x:A. Dec(

P(x)))

(A ~ ({x:A| P(x) }+{x:A|

P(x) }))

By:

Auto

Generated subgoal:

1 1. A : Type
2. P : AProp
3. x:A. Dec(P(x))
A ~ ({x:A| P(x) }+{x:A| P(x) })
4 steps

About:

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