Level: Lib Thy Top: 1 2
Hypotheses:

  1. q :

  2. x : q List

  3. q = 0

  4. u : q

  5. v : q List

Conclusion:

(u::v) = []

Applied Tactic: D 4 THEN Auto
Generated subgoals:

None