Nuprl - Pf lremove

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. St: Type
2. l: St*
3. s: St
4. eq: StSt
5. sx: St
6. u: St
7. v: St*
8. eq(s,sx)
9. mem_f(St;sx;v \ s) mem_f(St;sx;v)

mem_f(St;sx;(u.v) \ s) mem_f(St;sx;u.v)

By: RecUnfold `lremove` 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoals:

1 10. eq(s,u)
mem_f(St;sx;v \ s) (u = sx mem_f(St;sx;v))

2 10. eq(s,u)
mem_f(St;sx;u.(v \ s)) (u = sx mem_f(St;sx;v))

About:

1	10. `eq(s,u)` `mem_f(St;sx;v \ s) (u = sx mem_f(St;sx;v))`
2	10. `eq(s,u)` `mem_f(St;sx;u.(v \ s)) (u = sx mem_f(St;sx;v))`