Nuprl - Proof: union sigma inverses 1 2 1

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: union sigma inverses 1 2 1

1. A : Type
2. B : Type
3. i :

2
4. y1 : if i=

0

A else B fi

union_to_sigma(sigma_to_union(<i,y1>)) = <i,y1>

i:

2

if i=

0

A else B fi

By:	IntSegElim 3 THEN SplitITE Hyp:4 THEN Compute Counion_to_sigma(sigma_to_union(<i,y1>)) Costep:5: Co* CoInjCase(if i=0 inl(y1) else inr(y1) fi; a. <0,a>; b. <1,b>) THEN SplitITE Concl THEN Reduce Concl THEN Analyze

Generated subgoals:

None

About:

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

(7steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc