(3steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: find property 1

1. T : Type
2. P : T
3. T List
4. u : T
5. v : T List
6. d:T
6. ((first a  v s.t. P(a) else d v (first a  v s.t. P(a) else d) = d
7. P(u)
  d:T. (u  [u / v])  u = d


By: Auto THEN OrLeft THEN Easy


Generated subgoals:

None

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

(3steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc