Nuprl - Proof: union sigma inverses 1 2

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

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

if i=

A else B fi

union_to_sigma(sigma_to_union(y)) = y

By:

Analyze-1

Generated subgoal:

1 3. i : 2
4. y1 : if i=0 A else B fi
union_to_sigma(sigma_to_union(<i,y1>)) = <i,y1> i:2if i=0 A else B fi
1 step

About:

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