Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

St:. l:St List. s:St. eq:St St . l \ s St List

Applied Tactic: (RepD ...a)
Generated subgoals:

1. l \ s St List