Nuprl - Proof: card st vs msize 1 1 3

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card st vs msize 1 1 3

1. a :

2. P :

a

Prop
3. f :

a

2
4.

i:

a. P(i)

f(i) = 1
5. (

x.<x,0>)

{x:

a| P(x) }

(i:

a

(f(i)))
6. (

xi.xi/x,i. x)

(i:

a

(f(i)))

{x:

a| P(x) }

InvFuns({x:

a| P(x) };i:

a

(f(i));

x.<x,0>;

xi.xi/x,i. x)

By:	Analyze THEN Reduce Concl

Generated subgoal:

1 7. y : i:a(f(i))
<y/x,i. x,0> = y i:a(f(i))
2 steps

About:

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

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