Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
a:T.
bs:T List. mem_f(T;a;bs)
Applied Tactic:
(RepD THENM OnVar `bs' ListIndA THENM Reduce 0 ...)
Generated subgoals:
None
T:
. a:T. bs:T List. mem_f(T;a;bs) 
