(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sigma
to
union
wf
1
1.
A
: Type
2.
B
: Type
3.
i
:
2
4.
e1
: if
i
=
0
A
else
B
fi
if
i
=
0
inl(
e1
) else inr(
e1
) fi
A
+
B
By:
IntSegElim 3
Generated subgoals:
1
5.
i
= 0
2
if
i
=
0
inl(
e1
) else inr(
e1
) fi
A
+
B
2
steps
2
5.
i
= 1
2
if
i
=
0
inl(
e1
) else inr(
e1
) fi
A
+
B
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc