Level: Lib Thy Top: 1
Hypotheses:

  1. q :

  2. x : q List

  3. q = 0

Conclusion:

x = []

Applied Tactic: D 2
Generated subgoals:

1. [] = []

2. (u::v) = []