Nuprl - Pf list_in_mem_f

T:Type, as:T*. as {x:T| mem_f(T;x;as) }*

By: RepD THEN OnVar `as' ListIndA THEN Reduce 0

Generated subgoals:

1 1. T: Type
nil {T| False}*

2 1. T: Type
2. a: T
3. as: T*
4. as {x:T| mem_f(T;x;as) }*
a.as {x:T| a = x mem_f(T;x;as) }*

About:

1	1. `T:` `Type` `nil {T\| False}*`
2	1. `T:` `Type` 2. `a:` `T` 3. `as:` `T` 4. `as {x:T\| mem_f(T;x;as) }` `a.as {x:T\| a = x mem_f(T;x;as) }*`