Nuprl - Proof: card split decbl 1 1 1

(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc

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

1. A : Type
2. P : A

Prop
3.

x:A.

!i:

2. if i=

0

P(x) else

P(x) fi

A ~ (i:

2

if i=

0

{x:A| P(x) } else {x:A|

P(x) } fi)

By:	FwdThru: Thm* P:(ABProp). (x:A. !y:B. P(x;y)) (A ~ (y:B{x:A\| P(x;y) })) on [ Hyp:-1 ]

Generated subgoal:

1 4. A ~ (i:2{x:A| if i=0 P(x) else P(x) fi })
A ~ (i:2if i=0 {x:A| P(x) } else {x:A| P(x) } fi)
3 steps

About:

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

(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc