IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
union to sigma wf
A,B:Type. union_to_sigma
(A+B)
(i:
2
if i=
0
A else B fi)
By: |
Def of union_to_sigma |
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html