Nuprl - Pf lremove

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

St:Type, l:St*, s:St, eq:(StSt), sx:St. mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi

By: RepD THEN Analyze 0

Generated subgoals:

1 1. St: Type
2. l: St*
3. s: St
4. eq: StSt
5. sx: St
mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi

2 1. St: Type
2. l: St*
3. s: St
4. eq: StSt
5. sx: St
mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi

About:

1	1. `St:` `Type` 2. `l:` `St*` 3. `s:` `St` 4. `eq:` `StSt` 5. `sx:` `St` `mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi`
2	1. `St:` `Type` 2. `l:` `St*` 3. `s:` `St` 4. `eq:` `StSt` 5. `sx:` `St` `mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi`