(6steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sexpr cases wf
  A:Type, C:(Sexpr(A)Type), s:Sexpr(A), f:(s1,s2:Sexpr(A)C(Cons(s1;s2))),
  g:(x:AC(Inj(x))).
  (Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1,s2))  C(s)
By: Def of
Sexpr(A) |
Cons(<sexpr>;<sexpr>) |
Inj(<sexpr atom>) |
Case of <sexpr> :  Inj([var])  <atom case> ; Cons([var];[var])  <cons case>
THEN
UnivCD

Generated subgoals:

1 1. A : Type
2. C : rec(T.(TT)+A)Type
3. s : rec(T.(TT)+A)
4. f : s1,s2:rec(T.(TT)+A)C(inl(<s1,s2>))
5. g : x:AC(inr(x))
  InjCase(s; s1s2. s1s2/s1,s2. f(s1,s2); x. g(x))  C(s)
3 steps
2 1. A : Type
2. C : rec(T.(TT)+A)Type
3. rec(T.(TT)+A)
4. s1,s2:rec(T.(TT)+A)C(inl(<s1,s2>))
5. x : A
  inr(x)  rec(T.(TT)+A)
1 step
3 1. A : Type
2. rec(T.(TT)+A)Type
3. rec(T.(TT)+A)
4. s1 : rec(T.(TT)+A)
5. s2 : rec(T.(TT)+A)
  inl(<s1,s2>)  rec(T.(TT)+A)
1 step

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

(6steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc