(4steps total) PrintForm Definitions Lemmas hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq pred abstraction
  'a:Type, P:(('a'a)Prop).
  P(<eq_pred:(x:'a. y:'a. x = y)>)  (f:eq('a). P(f))
By: Unab [`eq_pred_marker`] THEN StrongAuto

Generated subgoals:

1 1. 'a : Type
2. P : ('a'a)Prop
3. P(x:'a. y:'a. x = y)
4. f : eq('a)
  P(f)
1 step
2 1. 'a : Type
2. P : ('a'a)Prop
3. f:eq('a). P(f)
  P(x:'a. y:'a. x = y)
2 steps

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

(4steps total) PrintForm Definitions Lemmas hol Sections HOLlib Doc