(2steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: add eq pred qf 1
1. 'a : Type
2. P : Prop
3. f:eq('a). P
  P
By: DTerm (x:'a. y:'a. x = y) 3 THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))
THEN
Analyze
THEN
StrongAuto
THEN
Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

(2steps total) PrintForm Definitions hol Sections HOLlib Doc