(4steps total)
PrintForm
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq
mem
is
ax
1
1
1.
A
: Type
2.
a
:
A
3.
a'
:
A
4.
a
=
a'
*
=
*
(
a
=
a'
)
By:
Refine RULE
H
*
=
*
(
a1
=
a2
A
) BY axiomEquality ;
H
a1
=
a2
A
[]
Generated subgoal:
1
a
=
a'
Hypothesis
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
DiscreteMath
Sections
DiscrMathExt
Doc
* = * 
(a = a') * = * (a = a') * = * (a1 = a2 A) BY axiomEquality ; H a1 = a2 A [] a = a'
