Nuprl - Pf lremove

1. St: Type
2. l: St*
3. s: St
4. eq: StSt
5. sx: St

mem_f(St;sx;nil \ s) if eq(s,sx) False else mem_f(St;sx;nil) fi

By: SplitOnConclITE THEN Analyze 0

Generated subgoals:

1 6. eq(s,sx)
7. False
mem_f(St;sx;nil \ s)

2 6. eq(s,sx)
7. mem_f(St;sx;nil)
mem_f(St;sx;nil \ s)

About:

1	6. `eq(s,sx)` 7. `False` `mem_f(St;sx;nil \ s)`
2	6. `eq(s,sx)` 7. `mem_f(St;sx;nil)` `mem_f(St;sx;nil \ s)`