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: RecUnfold `mem_f` 0 THEN RecUnfold `lremove` 0 THEN Reduce 0

Generated subgoals:

None

About: