Nuprl - Proof: card split prod intseg family decbl 1

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

1. A : Type
2. B : A

Type
3. P : A

Prop
4.

x:A. Dec(P(x))

(x:A

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

B(x))

(x:A st

P(x)

B(x)))

By:	Witness: h.<h,h>

Generated subgoal:

1 g:((x:A st P(x)B(x))(x:A st P(x)B(x))(x:AB(x))).
InvFuns(x:AB(x);(x:A st P(x)B(x))(x:A st P(x)B(x));h.<h,h>;g)
21 steps

About:

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