Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. as:T List. as {x:T| mem_f(T;x;as)} List

Applied Tactic: (RepD THENM OnVar `as' ListIndA THENM Reduce 0 ...a)
Generated subgoals:

1. [] {x:T| False} List

2. (a::as) {x:T| a = x mem_f(T;x;as)} List