(3steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
one
corr
2
reflex
A
:Type.
A
~
A
By:
UnivCD
{
We don't use Auto here because we're adding this lemma to the Auto tactic via
{
update_Auto_additions_for_ooc. }
Generated subgoal:
1
1.
A
: Type
A
~
A
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A:Type. A ~ A A:Type. A ~ A
We don't use Auto here because we're adding this lemma to the Auto tactic via
update_Auto_additions_for_ooc. } A ~ A
