(6steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bnot bexists

  T:S, P:(T). (x:TP(x)) = (x:TP(x))

By: Id THEN StrongAuto THEN Simpsetp [`bequal`] THEN StrongAuto


Generated subgoals:

1 1. T : S
2. P : T
3. (x:TP(x))
4. x : T
  P(x)

3 steps
2 1. T : S
2. P : T
3. x:TP(x)
  (x:TP(x))

2 steps

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

(6steps total) PrintForm Definitions hol Sections HOLlib Doc