Nuprl - Proof: card split prod intseg family decbl

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

A:Type, B:(A

Type), P:(A

Prop).

(

x:A. Dec(P(x)))

((x:A

B(x)) ~ ((x:A st P(x)

B(x))

(x:A st

P(x)

B(x))))

By:

UnivCD

Generated subgoal:

1 1. A : Type
2. B : AType
3. P : AProp
4. x:A. Dec(P(x))
(x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x)))
22 steps

About:

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