Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

St:. l:St List. eq:St St . LShort(l) St List

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

1. LShort(l) St List