(3steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-deq-member
  A:Type, eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L)
By: InductionOnList THEN Try (Reduce 0)

Generated subgoals:

1 1. A : Type
2. EqDecider(A)
3. A List
  x:A. false  (x  nil)
1 step
2 1. A : Type
2. eq : EqDecider(A)
3. A List
4. u : A
5. v : A List
6. x:A. deq-member(eq;x;v)  (x  v)
  x:A. (eqof(eq)(u,x)  deq-member(eq;x;v))  (x  [u / v])
1 step

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

(3steps total) PrintForm Definitions Lemmas mb event system 2 Sections EventSystems Doc